Reversible Computation in Term Rewriting

Abstract

Essentially, in a reversible programming language, for each forward computation from state $S$ to state $S^{\prime}$, there exists a constructive method to go backwards from state $S^{\prime}$ to state $S$. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few.

In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step $t_{1}\to t_{2}$, we do not always have a decidable method to get $t_{1}$ from $t_{2}$. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.

To appear in the Journal of Logical and Algebraic Methods in Programming.

1 Introduction

The notion of reversible computation can be traced back to Landauer’s pioneering work [22]. Although Landauer was mainly concerned with the energy consumption of erasing data in irreversible computing, he also claimed that every computer can be made reversible by saving the history of the computation. However, as Landauer himself pointed out, this would only postpone the problem of erasing the tape of a reversible Turing machine before it could be reused. Bennett [6] improved the original proposal so that the computation now ends with a tape that only contains the output of a computation and the initial source, thus deleting all remaining “garbage” data, though it performs twice the usual computation steps. More recently, Bennett’s result is extended in [9] to nondeterministic Turing machines, where it is also proved that transforming an irreversible Turing machine into a reversible one can be done with a quadratic loss of space. We refer the interested reader to, e.g., [7, 14, 40] for a high level account of the principles of reversible computation.

In the last decades, reversible computing and reversibilization (transforming an irreversible computation device into a reversible one) have been the subject of intense research, giving rise to successful applications in many different fields, e.g., cellular automata [28], where reversibility is an essential property, bidirectional program transformation [24], where reversibility helps to automate the generation of inverse functions (see Section 6), reversible debugging [17], where one can go both forward and backward when seeking the cause of an error, parallel discrete event simulation [34], where reversible computation is used to undo the effects of speculative computations made on a wrong assumption, quantum computing [39], where all computations should be reversible, and so forth. The interested reader can find detailed surveys in the state of the art reports of the different working groups of COST Action IC1405 on Reversible Computation [20].

In this work, we introduce reversibility in the context of term rewriting [4, 36], a computation model that underlies most rule-based programming languages. In contrast to other, more ad-hoc approaches, we consider that term rewriting is an excellent framework to rigorously define reversible computation in a functional context and formally prove its main properties. We expect our work to be useful in different (sequential) contexts, like reversible debugging, parallel discrete event simulation or bidirectional program transformation, to name a few. In particular, Section 6 presents a first approach to formalize bidirectional program transformation in our setting.

To be more precise, we present a general and intuitive notion of reversible term rewriting by defining a Landauer embedding. Given a rewrite system ${\mathcal{R}}$ and its associated (standard) rewrite relation $\to_{\mathcal{R}}$, we define a reversible extension of rewriting with two components: a forward relation $\mathrel{\rightharpoonup_{\mathcal{R}}}$ and a backward relation $\mathrel{\leftharpoondown_{\mathcal{R}}}$, such that $\mathrel{\rightharpoonup_{\mathcal{R}}}$ is a conservative extension of $\to_{\mathcal{R}}$ and, moreover, $\mathrel{(\rightharpoonup_{\mathcal{R}})^{-1}}\,=\,\mathrel{\leftharpoondown_{\mathcal{R}}}$. We note that the inverse rewrite relation, $\mathrel{(\to_{\mathcal{R}})^{-1}}$, is not an appropriate basis for “reversible” rewriting since we aim at defining a technique to undo a particular reduction. In other words, given a rewriting reduction $s\to^{\ast}_{\mathcal{R}}t$, our reversible relation aims at computing the term $s$ from $t$ and ${\mathcal{R}}$ in a decidable and deterministic way, which is not possible using $\mathrel{(\to_{\mathcal{R}})^{-1}}$ since it is generally non-deterministic, non-confluent, and non-terminating, even for systems defining injective functions (see Example 6). In contrast, our backward relation $\leftharpoondown_{\mathcal{R}}$ is deterministic (thus confluent) and terminating. Moreover, our relation proceeds backwards step by step, i.e., the number of reduction steps in $s\rightharpoonup^{\ast}_{\mathcal{R}}t$ and $t\leftharpoondown^{\ast}_{\mathcal{R}}s$ are the same.

In order to introduce a reversibilization transformation for rewrite systems, we use a flattening transformation so that the reduction at top positions of terms suffices to get a normal form in the transformed systems. For instance, given the following rewrite system:

$$\begin{array}[]{lrcll}&\mathsf{add}(\mathsf{0},y)&\to&y,{}\\ &\mathsf{add}(\mathsf{s}(x),y)&\to&\mathsf{s}(\mathsf{add}(x,y))&\\ \end{array}$$

defining the addition on natural numbers built from constructors $\mathsf{0}$ and $\mathsf{s}(~{})$, we produce the following flattened (conditional) system:

$$\begin{array}[]{lrcll}{\mathcal{R}}=\{&\mathsf{add}(\mathsf{0},y)&\to&y,\\ &\mathsf{add}(\mathsf{s}(x),y)&\to&\mathsf{s}(z)\Leftarrow\mathsf{add}(x,y)\twoheadrightarrow z&\}\\ \end{array}$$

(see Example 29 for more details). This allows us to provide an improved notion of reversible rewriting in which some information (namely, the positions where reduction takes place) is not required anymore. This opens the door to compile the reversible extension of rewriting into the system rules. Loosely speaking, given a system ${\mathcal{R}}$, we produce new systems ${\mathcal{R}}_{f}$ and ${\mathcal{R}}_{b}$ such that standard rewriting in ${\mathcal{R}}_{f}$, i.e., $\to_{{\mathcal{R}}_{f}}$, coincides with the forward reversible extension $\rightharpoonup_{\mathcal{R}}$ in the original system, and analogously $\to_{{\mathcal{R}}_{b}}$ is equivalent to $\leftharpoondown_{\mathcal{R}}$. E.g., for the system ${\mathcal{R}}$ above, we would produce

$$\begin{array}[]{l@{~}r@{~}c@{~}l@{~}l}{\mathcal{R}}_{f}=\{\hfil~{}&\mathsf{add}^{\mathtt{i}}(\mathsf{0},y)~{}&\to\hfil~{}&\langle y,\beta_{1}\rangle,\hfil~{}\\ \hfil~{}&\mathsf{add}^{\mathtt{i}}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\langle\mathsf{s}(z),\beta_{2}(w)\rangle\Leftarrow\mathsf{add}^{\mathtt{i}}(x,y)\twoheadrightarrow\langle z,w\rangle\hfil~{}&\}\\[8.61108pt] {\mathcal{R}}_{b}=\{\hfil~{}&\mathsf{add}^{-1}(y,\beta_{1})~{}&\to\hfil~{}&\langle\mathsf{0},y\rangle,\hfil~{}\\ \hfil~{}&\mathsf{add}^{-1}(\mathsf{s}(z),\beta_{2}(w))~{}&\to\hfil~{}&\langle\mathsf{s}(x),y\rangle\Leftarrow\mathsf{add}^{-1}(z,w)\to\langle x,y\rangle\hfil~{}&\}\end{array}$$

where $\mathsf{add}^{\mathtt{i}}$ is an injective version of function $\mathsf{add}$, $\mathsf{add}^{-1}$ is the inverse of $\mathsf{add}^{\mathtt{i}}$, and $\beta_{1},\beta_{2}$ are fresh symbols introduced to label the rules of ${\mathcal{R}}$.

In this work, we will mostly consider conditional rewrite systems, not only to have a more general notion of reversible rewriting, but also to define a reversibilization technique for unconditional rewrite systems, since the application of flattening (cf. Section 4) may introduce conditions in a system that is originally unconditional, as illustrated above.

This paper is an extended version of [31]. In contrast to [31], our current paper includes the proofs of technical results, the reversible extension of term rewriting is introduced first in the unconditional case (which is simpler and more intuitive), and presents an improved injectivization transformation when the system includes injective functions. Furthermore, a prototype implementation of the reversibilization technique is publicly available from http://kaz.dsic.upv.es/rev-rewriting.html.

The paper is organized as follows. After introducing some preliminaries in Section 2, we present our approach to reversible term rewriting in Section 3. Section 4 introduces the class of pure constructor systems where all reductions take place at topmost positions, so that storing this information in reversible rewrite steps becomes unnecessary. Then, Section 5 presents injectivization and inversion transformations in order to make a rewrite system reversible with standard rewriting. Here, we also present an improvement of the transformation for injective functions. The usefulness of these transformations is illustrated in Section 6. Finally, Section 7 discusses some related work and Section 8 concludes and points out some ideas for future research.

2 Preliminaries

We assume familiarity with basic concepts of term rewriting. We refer the reader to, e.g., [4] and [36] for further details.

2.1 Terms and Substitutions

A signature ${\mathcal{F}}$ is a set of ranked function symbols. Given a set of variables ${\mathcal{V}}$ with ${\mathcal{F}}\cap{\mathcal{V}}=\varnothing$, we denote the domain of terms by ${\mathcal{T}}({\mathcal{F}},{\mathcal{V}})$. We use $\mathsf{f},\mathsf{g},\ldots$ to denote functions and $x,y,\ldots$ to denote variables. Positions are used to address the nodes of a term viewed as a tree. A position $p$ in a term $t$, in symbols $p\in\mathsf{{{\cal P}}os}(t)$, is represented by a finite sequence of natural numbers, where $\epsilon$ denotes the root position. We let $t|_{p}$ denote the subterm of $t$ at position $p$ and $t[s]_{p}$ the result of replacing the subterm $t|_{p}$ by the term $s$. ${\mathcal{V}ar}(t)$ denotes the set of variables appearing in $t$. We also let ${\mathcal{V}ar}(t_{1},\ldots,t_{n})$ denote ${\mathcal{V}ar}(t_{1})\cup\cdots\cup{\mathcal{V}ar}(t_{n})$. A term $t$ is ground if ${\mathcal{V}ar}(t)=\varnothing$.

A substitution $\sigma:{\mathcal{V}}\mapsto{\mathcal{T}}({\mathcal{F}},{\mathcal{V}})$ is a mapping from variables to terms such that $\mathsf{{{\mathcal{D}}}om}(\sigma)=\{x\in{\mathcal{V}}\mid x\neq\sigma(x)\}$ is its domain. A substitution $\sigma$ is ground if $x\sigma$ is ground for all $x\in\mathsf{{{\mathcal{D}}}om}(\sigma)$. Substitutions are extended to morphisms from ${\mathcal{T}}({\mathcal{F}},{\mathcal{V}})$ to ${\mathcal{T}}({\mathcal{F}},{\mathcal{V}})$ in the natural way. We denote the application of a substitution $\sigma$ to a term $t$ by $t\sigma$ rather than $\sigma(t)$. The identity substitution is denoted by $id$. We let “$\circ$” denote the composition of substitutions, i.e., $\sigma\circ\theta(x)=(x\theta)\sigma=x\theta\sigma$. The restriction $\theta\!\mathrel{|\grave{}}_{V}$ of a substitution $\theta$ to a set of variables $V$ is defined as follows: $x\theta\!\mathrel{|\grave{}}_{V}=x\theta$ if $x\in V$ and $x\theta\!\mathrel{|\grave{}}_{V}=x$ otherwise.

2.2 Term Rewriting Systems

A set of rewrite rules $l\to r$ such that $l$ is a nonvariable term and $r$ is a term whose variables appear in $l$ is called a term rewriting system (TRS for short); terms $l$ and $r$ are called the left-hand side and the right-hand side of the rule, respectively. We restrict ourselves to finite signatures and TRSs. Given a TRS ${\mathcal{R}}$ over a signature ${\mathcal{F}}$, the defined symbols ${\mathcal{D}}_{\mathcal{R}}$ are the root symbols of the left-hand sides of the rules and the constructors are ${\mathcal{C}}_{\mathcal{R}}={\mathcal{F}}\;\backslash\;{\mathcal{D}}_{\mathcal{R}}$. Constructor terms of ${\mathcal{R}}$ are terms over ${\mathcal{C}}_{\mathcal{R}}$ and ${\mathcal{V}}$, denoted by ${\mathcal{T}}({\mathcal{C}}_{\mathcal{R}},{\mathcal{V}})$. We sometimes omit ${\mathcal{R}}$ from ${\mathcal{D}}_{\mathcal{R}}$ and ${\mathcal{C}}_{\mathcal{R}}$ if it is clear from the context. A substitution $\sigma$ is a constructor substitution (of ${\mathcal{R}}$) if $x\sigma\in{\mathcal{T}}({\mathcal{C}}_{\mathcal{R}},{\mathcal{V}})$ for all variables $x$.

For a TRS ${\mathcal{R}}$, we define the associated rewrite relation $\to_{\mathcal{R}}$ as the smallest binary relation on terms satisfying the following: given terms $s,t\in{\mathcal{T}}({\mathcal{F}},{\mathcal{V}})$, we have $s\to_{\mathcal{R}}t$ iff there exist a position $p$ in $s$, a rewrite rule $l\to r\in{\mathcal{R}}$, and a substitution $\sigma$ such that $s|_{p}=l\sigma$ and $t=s[r\sigma]_{p}$; the rewrite step is sometimes denoted by $s\to_{p,l\to r}t$ to make explicit the position and rule used in this step. The instantiated left-hand side $l\sigma$ is called a redex. A term $s$ is called irreducible or in normal form with respect to a TRS ${\mathcal{R}}$ if there is no term $t$ with $s\to_{\mathcal{R}}t$. A substitution is called normalized with respect to ${\mathcal{R}}$ if every variable in the domain is replaced by a normal form with respect to ${\mathcal{R}}$. We sometimes omit “with respect to ${\mathcal{R}}$” if it is clear from the context. A derivation is a (possibly empty) sequence of rewrite steps. Given a binary relation $\to$, we denote by $\rightarrow^{\ast}$ its reflexive and transitive closure, i.e., $s\to^{\ast}_{\mathcal{R}}t$ means that $s$ can be reduced to $t$ in ${\mathcal{R}}$ in zero or more steps; we also use $s\to^{n}_{\mathcal{R}}t$ to denote that $s$ can be reduced to $t$ in exactly $n$ steps.

We further assume that rewrite rules are labelled, i.e., given a TRS ${\mathcal{R}}$, we denote by $\beta:l\to r$ a rewrite rule with label $\beta$. Labels are unique in a TRS. Also, to relate label $\beta$ to fixed variables, we consider that the variables of the rewrite rules are not renamed and that the reduced terms are always ground. Equivalently, one could require terms to be variable disjoint with the variables of the rewrite system, but we require groundness for simplicity. We often write $s\to_{p,\beta}t$ instead of $s\to_{p,l\to r}t$ if rule $l\to r$ is labeled with $\beta$.

2.3 Conditional Term Rewrite Systems

In this paper, we also consider conditional term rewrite systems (CTRSs); namely oriented 3-CTRSs, i.e., CTRSs where extra variables are allowed as long as ${\mathcal{V}ar}(r)\subseteq{\mathcal{V}ar}(l)\cup{\mathcal{V}ar}(C)$ for any rule $l\to r\Leftarrow C$ [26]. In oriented CTRSs, a conditional rule $l\to r\Leftarrow C$ has the form $l\to r\Leftarrow s_{1}\twoheadrightarrow t_{1},\ldots,s_{n}\twoheadrightarrow t_{n}$, where each oriented equation $s_{i}\twoheadrightarrow t_{i}$ is interpreted as reachability ($\to_{\mathcal{R}}^{\ast}$). In the following, we denote by $\overline{o_{n}}$ a sequence of elements $o_{1},\ldots,o_{n}$ for some $n$. We also write $\overline{o_{i,j}}$ for the sequence $o_{i},\ldots,o_{j}$ when $i\leq j$ (and the empty sequence otherwise). We write $\overline{o}$ when the number of elements is not relevant. In addition, we denote a condition $o_{1}\twoheadrightarrow o^{\prime}_{1},\ldots,o_{n}\twoheadrightarrow o^{\prime}_{n}$ by $\overline{o_{n}\twoheadrightarrow o^{\prime}_{n}}$.

As in the unconditional case, we consider that rules are labelled and that labels are unique in a CTRS. And, again, to relate label $\beta$ to fixed variables, we consider that the variables of the conditional rewrite rules are not renamed and that the reduced terms are always ground.

For a CTRS ${\mathcal{R}}$, the associated rewrite relation $\to_{\mathcal{R}}$ is defined as the smallest binary relation satisfying the following: given ground terms $s,t\in{\mathcal{T}}({\mathcal{F}})$, we have $s\to_{\mathcal{R}}t$ iff there exist a position $p$ in $s$, a rewrite rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s|_{p}=l\sigma$, $s_{i}\sigma\to^{\ast}_{\mathcal{R}}t_{i}\sigma$ for all $i=1,\ldots,n$, and $t=s[r\sigma]_{p}$.

In order to simplify the presentation, we only consider deterministic CTRSs (DCTRSs), i.e., oriented 3-CTRSs where, for each rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}$, we have $\mathsf{{{\mathcal{V}}}ar}(s_{i})\subseteq\mathsf{{{\mathcal{V}}}ar}(l,\overline{t_{i-1}})$ for all $i=1,\ldots,n$ (see Section 3.2 for a justification of this requirement and how it could be relaxed to arbitrary 3-CTRSs). Intuitively speaking, the use of DCTRs allows us to compute the bindings for the variables in the condition of a rule in a deterministic way. E.g., given a ground term $s$ and a rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}$ with $s|_{p}=l\theta$, we have that $s_{1}\theta$ is ground. Therefore, one can reduce $s_{1}\theta$ to some term $s^{\prime}_{1}$ such that $s^{\prime}_{1}$ is an instance of $t_{1}\theta$ with some ground substitution $\theta_{1}$. Now, we have that $s_{2}\theta\theta_{1}$ is ground and we can reduce $s_{2}\theta\theta_{1}$ to some term $s^{\prime}_{2}$ such that $s^{\prime}_{2}$ is an instance of $t_{2}\theta\theta_{1}$ with some ground substitution $\theta_{2}$, and so forth. If all equations in the condition hold using $\theta_{1},\ldots,\theta_{n}$, we have that $s\to_{p,\beta}s[r\sigma]_{p}$ with $\sigma=\theta\theta_{1}\ldots\theta_{n}$.

Example 1

Consider the following DCTRS ${\mathcal{R}}$ that defines the function $\mathsf{double}$ that doubles the value of its argument when it is an even natural number:

$$\begin{array}[]{l@{~}r@{~}c@{~}l@{}l@{~}r@{~}c@{~}l}\beta_{1}:\hfil~{}&\mathsf{add}(\mathsf{0},y)~{}&\to\hfil~{}&y&\beta_{4}:\hfil~{}&\mathsf{even}(\mathsf{0})~{}&\to\hfil~{}&\mathsf{true}\\ \beta_{2}:\hfil~{}&\mathsf{add}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\mathsf{s}(\mathsf{add}(x,y))&\beta_{5}:\hfil~{}&\mathsf{even}(\mathsf{s}(\mathsf{s}(x)))~{}&\to\hfil~{}&\mathsf{even}(x)\\ \beta_{3}:\hfil~{}&\mathsf{double}(x)~{}&\to\hfil~{}&\mathsf{add}(x,x)\Leftarrow\mathsf{even}(x)\twoheadrightarrow\mathsf{true}\\ \end{array}$$

Given the term $\mathsf{double}(\mathsf{s}(\mathsf{s}(\mathsf{0})))$ we have, for instance, the following derivation:

$$\begin{array}[]{l@{}l@{}lll}\mathsf{double}(\mathsf{s}(\mathsf{s}(\mathsf{0})))&\to_{\epsilon,\beta_{3}}&\mathsf{add}(\mathsf{s}(\mathsf{s}(\mathsf{0})),\mathsf{s}(\mathsf{s}(\mathsf{0})))&\mbox{since}~{}\mathsf{even}(\mathsf{s}(\mathsf{s}(\mathsf{0})))\to_{\mathcal{R}}^{\ast}\mathsf{true}\\ &&&\mbox{with}~{}\sigma=\{x\mapsto\mathsf{s}(\mathsf{s}(\mathsf{0}))\}\\ &\to_{\epsilon,\beta_{2}}&\mathsf{s}(\mathsf{add}(\mathsf{s}(\mathsf{0}),\mathsf{s}(\mathsf{s}(\mathsf{0}))))&\mbox{with}~{}\sigma=\{x\mapsto\mathsf{s}(\mathsf{0}),~{}y\mapsto\mathsf{s}(\mathsf{s}(\mathsf{0}))\}\\ &\to_{1,\beta_{2}}&\mathsf{s}(\mathsf{s}(\mathsf{add}(\mathsf{0},\mathsf{s}(\mathsf{s}(\mathsf{0})))))&\mbox{with}~{}\sigma=\{x\mapsto\mathsf{0},y\mapsto\mathsf{s}(\mathsf{s}(\mathsf{0}))\}\\ &\to_{1.1,\beta_{1}}&\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{0}))))&\mbox{with}~{}\sigma=\{y\mapsto\mathsf{s}(\mathsf{s}(\mathsf{0}))\}\end{array}$$

3 Reversible Term Rewriting

In this section, we present a conservative extension of the rewrite relation which becomes reversible. In the following, we use $\rightharpoonup_{\mathcal{R}}$ to denote our reversible (forward) term rewrite relation, and $\leftharpoondown_{\mathcal{R}}$ to denote its application in the reverse (backward) direction. Note that, in principle, we do not require $\leftharpoondown_{\mathcal{R}}\>=\>\rightharpoonup_{\mathcal{R}}^{-1}$, i.e., we provide independent (constructive) definitions for each relation. Nonetheless, we will prove that $\leftharpoondown_{\mathcal{R}}\>=\>\rightharpoonup_{\mathcal{R}}^{-1}$ indeed holds (cf. Theorems 9 and 20). In some approaches to reversible computing, both forward and backward relations should be deterministic. Here, we will only require deterministic backward steps, while forward steps might be non-deterministic, as it is often the case in term rewriting.

3.1 Unconditional Term Rewrite Systems

We start with unconditional TRSs since it is conceptually simpler and thus will help the reader to better understand the key ingredients of our approach. In the next section, we will consider the more general case of DCTRSs.

Given a TRS ${\mathcal{R}}$, reversible rewriting is defined on pairs $\langle t,\pi\rangle$, where $t$ is a ground term and $\pi$ is a trace (the “history” of the computation so far). Here, a trace in ${\mathcal{R}}$ is a list of trace terms of the form $\beta(p,\sigma)$ such that $\beta$ is a label for some rule $l\to r\in{\mathcal{R}}$, $p$ is a position, and $\sigma$ is a substitution with $\mathsf{{{\mathcal{D}}}om}(\sigma)=\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)$ which will record the bindings of erased variables when $\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)\neq\varnothing$ (and $\sigma=id$ if $\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)=\varnothing$). Our trace terms have some similarities with proof terms [36]. However, proof terms do not store the bindings of erased variables (and, to the best of our knowledge, they are only defined for unconditional TRSs, while we use trace terms both for unconditional and conditional TRSs).

Our reversible term rewriting relation is only defined on safe pairs:

Definition 2

Let ${\mathcal{R}}$ be a TRS. The pair $\langle s,\pi\rangle$ is safe in ${\mathcal{R}}$ iff, for all $\beta(p,\sigma)$ in $\pi$, $\sigma$ is a ground substitution with $\mathsf{{{\mathcal{D}}}om}(\sigma)=\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)$ and $\beta:l\to r\in{\mathcal{R}}$.

In the following, we often omit ${\mathcal{R}}$ when referring to traces and safe pairs if the underlying TRS is clear from the context.

Safety is not necessary when applying a forward reduction step, but will become essential for the backward relation $\leftharpoondown_{\mathcal{R}}$ to be correct. E.g., all traces that come from the forward reduction of some initial pair with an empty trace will be safe (see below). Reversible rewriting is then introduced as follows:

Definition 3

Let ${\mathcal{R}}$ be a TRS. A reversible rewrite relation $\rightharpoonup_{\mathcal{R}}$ is defined on safe pairs $\langle t,\pi\rangle$, where $t$ is a ground term and $\pi$ is a trace in ${\mathcal{R}}$. The reversible rewrite relation extends standard rewriting as follows:

$$\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}\langle t,\beta(p,\sigma^{\prime}):\pi\rangle$$

iff there exist a position $p\in\mathsf{{{\cal P}}os}(s)$, a rewrite rule $\beta:l\to r\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s|_{p}=l\sigma$, $t=s[r\sigma]_{p}$, and $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)}$. The reverse relation, $\leftharpoondown_{\mathcal{R}}$, is then defined as follows:

$$\langle t,\beta(p,\sigma^{\prime}):\pi\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$$

iff $\langle t,\beta(p,\sigma^{\prime}):\pi\rangle$ is a safe pair in ${\mathcal{R}}$ and there exist a ground substitution $\theta$ and a rule $\beta:l\to r\in{\mathcal{R}}$ such that $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r)$, $t|_{p}=r\theta$ and $s=t[l\theta\sigma^{\prime}]_{p}$. Note that $\theta\sigma^{\prime}=\sigma^{\prime}\theta=\theta\cup\sigma^{\prime}$, where $\cup$ is the union of substitutions, since $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r)$, $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r))$ and both substitutions are ground, so $\mathsf{{{\mathcal{D}}}om}(\theta)\cap\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\varnothing$.

We denote the union of both relations $\rightharpoonup_{\mathcal{R}}\cup\leftharpoondown_{\mathcal{R}}$ by $\rightleftharpoons_{\mathcal{R}}$.

Example 4

Let us consider the following TRS ${\mathcal{R}}$ defining the addition on natural numbers built from $\mathsf{0}$ and $\mathsf{s}(~{})$, and the function $\mathsf{fst}$ that returns its first argument:

$$\begin{array}[]{lrcl@{~~~~~~~~~~}lrcl}\beta_{1}:&\mathsf{add}(\mathsf{0},y)&\to&y\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}&\beta_{3}:&\mathsf{fst}(x,y)&\to&x\\ \beta_{2}:&\mathsf{add}(\mathsf{s}(x),y)&\to&\mathsf{s}(\mathsf{add}(x,y))\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}~{}\\ \end{array}$$

Given the term $\mathsf{fst}(\mathsf{add}(\mathsf{s}(\mathsf{0}),\mathsf{0}),\mathsf{0})$, we have, for instance, the following reversible (forward) derivation:

$$\begin{array}[]{lll}\langle\mathsf{fst}(\mathsf{add}(\mathsf{s}(\mathsf{0}),\mathsf{0}),\mathsf{0}),{\color[rgb]{0,0,0}[\,]}\rangle&\rightharpoonup_{\mathcal{R}}&\langle\mathsf{fst}(\mathsf{s}(\mathsf{add}(\mathsf{0},\mathsf{0})),\mathsf{0}),{\color[rgb]{0,0,0}[\beta_{2}(1,id)]}\rangle\\ &\rightharpoonup_{\mathcal{R}}&\langle\mathsf{s}(\mathsf{add}(\mathsf{0},\mathsf{0})),{\color[rgb]{0,0,0}[\beta_{3}(\epsilon,\{y\mapsto\mathsf{0}\}),\beta_{2}(1,id)]}\rangle\\ &\rightharpoonup_{\mathcal{R}}&\langle\mathsf{s}(\mathsf{0}),{\color[rgb]{0,0,0}[\beta_{1}(1,id),\beta_{3}(\epsilon,\{y\mapsto\mathsf{0}\}),\beta_{2}(1,id)]}\rangle\\ \end{array}$$

The reader can easily check that $\langle\mathsf{s}(\mathsf{0}),{\color[rgb]{0,0,0}[\beta_{1}(1,id),\beta_{3}(\epsilon,\{y\mapsto\mathsf{0}\}),\beta_{2}(1,id)]}\rangle$ is reducible to $\langle\mathsf{fst}(\mathsf{add}(\mathsf{s}(\mathsf{0}),\mathsf{0}),\mathsf{0}),{\color[rgb]{0,0,0}[\,]}\rangle$ using the backward relation $\leftharpoondown_{\mathcal{R}}$ by performing exactly the same steps but in the backward direction.

An easy but essential property of $\rightharpoonup_{\mathcal{R}}$ is that it is a conservative extension of standard rewriting in the following sense (we omit its proof since it is straightforward):

Theorem 5

Let ${\mathcal{R}}$ be a TRS. Given terms $s,t$, if $s\to_{\mathcal{R}}^{\ast}t$, then for any trace $\pi$ there exists a trace $\pi^{\prime}$ such that $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}^{\ast}\langle t,\pi^{\prime}\rangle$.

Here, and in the following, we assume that $\mathrel{\leftarrow_{\mathcal{R}}}\,=\,\mathrel{(\to_{\mathcal{R}})^{-1}}$, i.e., $s\to_{\mathcal{R}}^{-1}t$ is denoted by $s\mathrel{\leftarrow_{\mathcal{R}}}t$. Observe that the backward relation is not a conservative extension of $\mathrel{\leftarrow_{\mathcal{R}}}$: in general, $t\leftarrow_{\mathcal{R}}s$ does not imply $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$ for any arbitrary trace $\pi^{\prime}$. This is actually the purpose of our notion of reversible rewriting: $\leftharpoondown_{\mathcal{R}}$ should not extend $\leftarrow_{\mathcal{R}}$ but is only aimed at performing exactly the same steps of the forward computation whose trace was stored, but in the reverse order. Nevertheless, one can still ensure that for all steps $t\leftarrow_{\mathcal{R}}s$, there exists some trace $\pi^{\prime}$ such that $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$ (which is an easy consequence of the above result and Theorem 9 below).

Example 6

Consider again the following TRS ${\mathcal{R}}=\{\beta:~{}\mathsf{snd}(x,y)\to y\}$. Given the reduction $\mathsf{snd}(\mathsf{1},\mathsf{2})\to_{\mathcal{R}}\mathsf{2}$, there are infinitely many reductions for $\mathsf{\mathsf{2}}$ using $\leftarrow_{\mathcal{R}}$, e.g., $\mathsf{2}\leftarrow_{\mathcal{R}}\mathsf{snd}(\mathsf{1},\mathsf{2})$, $\mathsf{2}\leftarrow_{\mathcal{R}}\mathsf{snd}(\mathsf{2},\mathsf{2})$, $\mathsf{2}\leftarrow_{\mathcal{R}}\mathsf{snd}(\mathsf{3},\mathsf{2})$, etc. The relation is also non-terminating: $\mathsf{2}\leftarrow_{\mathcal{R}}\mathsf{snd}(\mathsf{1},\mathsf{2})\leftarrow_{\mathcal{R}}\mathsf{snd}(\mathsf{1},\mathsf{snd}(\mathsf{1},\mathsf{2}))\leftarrow_{\mathcal{R}}\cdots$. In contrast, given a pair $\langle\mathsf{2},\pi\rangle$, we can only perform a single deterministic and finite reduction (as proved below). For instance, if $\pi=[\beta(\epsilon,\{x\mapsto\mathsf{\mathsf{1}}\}),\beta({2},\{x\mapsto\mathsf{\mathsf{1}}\})]$, then the only possible reduction is $\langle\mathsf{\mathsf{2}},\pi\rangle\leftharpoondown_{\mathcal{R}}\langle\mathsf{snd}(\mathsf{\mathsf{1}},\mathsf{\mathsf{2}}),[\beta({2},\{x\mapsto\mathsf{\mathsf{1}}\})]\rangle\leftharpoondown_{\mathcal{R}}\langle\mathsf{snd}(\mathsf{\mathsf{1}},\mathsf{snd}(\mathsf{\mathsf{1}},\mathsf{\mathsf{2}})),[\,]\rangle\not\leftharpoondown_{\mathcal{R}}$.

Now, we state a lemma which shows that safe pairs are preserved through reversible term rewriting (both in the forward and backward directions):

Lemma 7

Let ${\mathcal{R}}$ be a TRS. Let $\langle s,\pi\rangle$ be a safe pair. If $\langle s,\pi\rangle\rightleftharpoons^{\ast}_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$, then $\langle t,\pi^{\prime}\rangle$ is also safe.

Proof 1

We prove the claim by induction on the length $k$ of the derivation. Since the base case $k=0$ is trivial, consider the inductive case $k>0$. Assume a derivation of the form $\langle s,\pi\rangle\rightleftharpoons_{\mathcal{R}}^{\ast}\langle s_{0},\pi_{0}\rangle\rightleftharpoons_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$. By the induction hypothesis, we have that $\langle s_{0},\pi_{0}\rangle$ is a safe pair. Now, we distinguish two cases depending on the last step. If we have $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$, then there exist a position $p\in\mathsf{{{\cal P}}os}(s_{0})$, a rewrite rule $\beta:l\to r\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s_{0}|_{p}=l\sigma$, $t=s_{0}[r\sigma]_{p}$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)}$, and $\pi^{\prime}=\beta(p,\sigma^{\prime}):\pi_{0}$. Then, since $\sigma^{\prime}$ is ground and $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)$ by construction, the claim follows straightforwardly. If the last step has the form $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$, then the claim follows trivially since each step with $\leftharpoondown_{\mathcal{R}}$ only removes trace terms from $\pi_{0}$.

Hence, since any pair with an empty trace is safe the following result, which states that every pair that is reachable from an initial pair with an empty trace is safe, straightforwardly follows from Lemma 7:

Proposition 8

Let ${\mathcal{R}}$ be a TRS. If $\langle s,[\,]\rangle\rightleftharpoons_{\mathcal{R}}^{\ast}\langle t,\pi\rangle$, then $\langle t,\pi\rangle$ is safe.

Now, we state the reversibility of $\rightharpoonup_{\mathcal{R}}$, i.e., the fact that $(\rightharpoonup_{\mathcal{R}})^{-1}=\>\leftharpoondown_{\mathcal{R}}$ (and thus the reversibility of $\leftharpoondown_{\mathcal{R}}$ and $\rightleftharpoons_{\mathcal{R}}$, too).

Theorem 9

Let ${\mathcal{R}}$ be a TRS. Given the safe pairs $\langle s,\pi\rangle$ and $\langle t,\pi^{\prime}\rangle$, for all $n\geq 0$, $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}^{n}\langle t,\pi^{\prime}\rangle$ iff $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}^{n}\langle s,\pi\rangle$.

Proof 2

$(\Rightarrow)$ We prove the claim by induction on the length $n$ of the derivation $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}^{n}\langle t,\pi^{\prime}\rangle$. Since the base case $n=0$ is trivial, let us consider the inductive case $n>0$. Consider a derivation $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}^{n-1}\langle s_{0},\pi_{0}\rangle\rightharpoonup_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$. By Lemma 7, both $\langle s_{0},\pi_{0}\rangle$ and $\langle t,\pi^{\prime}\rangle$ are safe. By the induction hypothesis, we have $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{\mathcal{R}}^{n-1}\langle s,\pi\rangle$. Consider now the step $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{\mathcal{R}}\langle t,\pi^{\prime}\rangle$. Then, there is a position $p\in\mathsf{{{\cal P}}os}(s_{0})$, a rule $\beta:l\to r\in{\mathcal{R}}$ and a ground substitution $\sigma$ such that $s_{0}|_{p}=l\sigma$, $t=s_{0}[r\sigma]_{p}$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)}$, and $\pi^{\prime}=\beta(p,\sigma^{\prime}):\pi_{0}$. Let $\theta=\sigma\!\!\mathrel{|\grave{}}_{\mathsf{{{\mathcal{V}}}ar}(r)}$. Then, we have $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s^{\prime}_{0},\pi_{0}\rangle$ with $t|_{p}=r\theta$, $\beta:l\to r\in{\mathcal{R}}$ and $s^{\prime}_{0}=t[l\theta\sigma^{\prime}]_{p}$. Moreover, since $\sigma=\theta\sigma^{\prime}$, we have $s^{\prime}_{0}=t[l\theta\sigma^{\prime}]_{p}=t[l\sigma]_{p}=s_{0}$, and the claim follows.

$(\Leftarrow)$ This direction proceeds in a similar way. We prove the claim by induction on the length $n$ of the derivation $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}^{n}\langle s,\pi\rangle$. As before, we only consider the inductive case $n>0$. Let us consider a derivation $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}^{n-1}\langle s_{0},\pi_{0}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$. By Lemma 7, both $\langle s_{0},\pi_{0}\rangle$ and $\langle s,\pi\rangle$ are safe. By the induction hypothesis, we have $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{\mathcal{R}}^{n-1}\langle t,\pi^{\prime}\rangle$. Consider now the reduction step $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$. Then, we have $\pi_{0}=\beta(p,\sigma^{\prime}):\pi$, $\beta:l\to r\in{\mathcal{R}}$, and there exists a ground substitution $\theta$ with $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r)$ such that $s_{0}|_{p}=r\theta$ and $s=s_{0}[l\theta\sigma^{\prime}]_{p}$. Moreover, since $\langle s_{0},\pi_{0}\rangle$ is safe, we have that $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)$ and, thus, $\mathsf{{{\mathcal{D}}}om}(\theta)\cap\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\varnothing$. Let $\sigma=\theta\sigma^{\prime}$. Then, since $s|_{p}=l\sigma$ and $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r)$, we can perform the step $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}\langle s^{\prime}_{0},\beta(p,\sigma^{\prime}):\pi\rangle$ with $s^{\prime}_{0}=s[r\sigma]_{p}=s[r\theta\sigma^{\prime}]_{p}=s[r\theta]_{p}=s_{0}[r\theta]_{p}=s_{0}$, and the claim follows.

The next corollary is then immediate:

Corollary 10

Let ${\mathcal{R}}$ be a TRS. Given the safe pairs $\langle s,\pi\rangle$ and $\langle t,\pi^{\prime}\rangle$, for all $n\geq 0$, $\langle s,\pi\rangle\rightleftharpoons_{\mathcal{R}}^{n}\langle t,\pi^{\prime}\rangle$ iff $\langle t,\pi^{\prime}\rangle\rightleftharpoons_{\mathcal{R}}^{n}\langle s,\pi\rangle$.

A key issue of our notion of reversible rewriting is that the backward rewrite relation $\leftharpoondown_{\mathcal{R}}$ is deterministic (thus confluent), terminating, and has a constructive definition:

Theorem 11

Let ${\mathcal{R}}$ be a TRS. Given a safe pair $\langle t,\pi^{\prime}\rangle$, there exists at most one pair $\langle s,\pi\rangle$ such that $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$.

Proof 3

First, if there is no step using $\leftharpoondown_{\mathcal{R}}$ from $\langle t,\pi^{\prime}\rangle$, the claim follows trivially. Now, assume there is at least one step $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$. We prove that this is the only possible step. By definition, we have $\pi^{\prime}=\beta(p,\sigma^{\prime}):\pi$, $p\in\mathsf{{{\cal P}}os}(t)$, $\beta:l\to r\in{\mathcal{R}}$, and there exists a ground substitution $\theta$ with $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r)$ such that $t|_{p}=r\theta$ and $s=t[l\theta\sigma^{\prime}]_{p}$. The only source of nondeterminism may come from choosing a rule labeled with $\beta$ and from the computation of the substitution $\theta$. The claim follows trivially from the fact that labels are unique in ${\mathcal{R}}$ and that, if there is some ground substitution $\theta^{\prime}$ with $\theta^{\prime}=\mathsf{{{\mathcal{V}}}ar}(r)$ and $t|_{p}=r\theta^{\prime}$, then $\theta=\theta^{\prime}$.

Therefore, $\leftharpoondown_{\mathcal{R}}$ is clearly deterministic and confluent. Termination holds straightforwardly for pairs with finite traces since its length strictly decreases with every backward step. Note however that even when $\rightharpoonup_{\mathcal{R}}$ and $\leftharpoondown_{\mathcal{R}}$ are terminating, the relation $\rightleftharpoons_{\mathcal{R}}$ is always non-terminating since one can keep going back and forth.

3.2 Conditional Term Rewrite Systems

In this section, we extend the previous notions and results to DCTRSs. We note that considering DCTRSs is not enough to make conditional rewriting deterministic. In general, given a rewrite step $s\to_{p,\beta}t$ with $p$ a position of $s$, $\beta:l\to r\Leftarrow\overline{s_{n}\to t_{n}}$ a rule, and $\sigma$ a substitution such that $s|_{p}=l\sigma$ and $s_{i}\sigma\to^{\ast}_{\mathcal{R}}t_{i}\sigma$ for all $i=1,\ldots,n$, there are three potential sources of non-determinism: the selected position $p$, the selected rule $\beta$, and the substitution $\sigma$. The use of DCTRSs can only make deterministic the last one, but the choice of a position and the selection of a rule may still be non-deterministic.

For DCTRSs, the notion of a trace term used for TRSs is not sufficient since we also need to store the traces of the subderivations associated to the condition of the applied rule (if any). Therefore, we generalize the notion of a trace as follows:

Definition 12 (trace)

Given a CTRS ${\mathcal{R}}$, a trace in ${\mathcal{R}}$ is recursively defined as follows:

• the empty list is a trace;

• if $\pi,\pi_{1},\ldots,\pi_{n}$ are traces in ${\mathcal{R}}$, $n\geq 0$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$ is a rule, $p$ is a position, and $\sigma$ is a ground substitution, then $\beta(p,\sigma,\pi_{1},\ldots,\pi_{n}):\pi$ is a trace in ${\mathcal{R}}$.

We refer to each component $\beta(p,\sigma,\pi_{1},\ldots,\pi_{n})$ in a trace as a trace term.

Intuitively speaking, a trace term $\beta(p,\sigma,\pi_{1},\ldots,\pi_{n})$ stores the position of a reduction step, a substitution with the bindings that are required for the step to be reversible (e.g., the bindings for the erased variables, but not only; see below) and the traces associated to the subcomputations in the condition.

The notion of a safe pair is now more involved in order to deal with conditional rules. The motivation for this definition will be explained below, after introducing reversible rewriting for DCTRSs.

Definition 13 (safe pair)

Let ${\mathcal{R}}$ be a DCTRS. A trace $\pi$ is safe in ${\mathcal{R}}$ iff, for all trace terms $\beta(p,\sigma,\overline{\pi_{n}})$ in $\pi$, $\sigma$ is a ground substitution with $\mathsf{{{\mathcal{D}}}om}(\sigma)=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and $\overline{\pi_{n}}$ are safe too. The pair $\langle s,\pi\rangle$ is safe in ${\mathcal{R}}$ iff $\pi$ is safe.

Reversible (conditional) rewriting can now be introduced as follows:

Definition 14 (reversible rewriting)

Let ${\mathcal{R}}$ be a DCTRS. The reversible rewrite relation $\rightharpoonup_{\mathcal{R}}$ is defined on safe pairs $\langle t,\pi\rangle$, where $t$ is a ground term and $\pi$ is a trace in ${\mathcal{R}}$. The reversible rewrite relation extends standard conditional rewriting as follows:

$$\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}\langle t,\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi\rangle$$

iff there exist a position $p\in\mathsf{{{\cal P}}os}(s)$, a rewrite rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s|_{p}=l\sigma$, $\langle s_{i}\sigma,[\,]\rangle\rightharpoonup_{\mathcal{R}}^{\ast}\langle t_{i}\sigma,\pi_{i}\rangle$ for all $i=1,\ldots,n$, $t=s[r\sigma]_{p}$, and $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$. The reverse relation, $\leftharpoondown_{\mathcal{R}}$, is then defined as follows:

$$\langle t,\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$$

iff $\langle t,\beta(p,\sigma^{\prime},\overline{\pi_{n}}):\pi\rangle$ is a safe pair in ${\mathcal{R}}$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$ and there is a ground substitution $\theta$ such that $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}})\backslash\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})$, $t|_{p}=r\theta$, $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle\leftharpoondown_{\mathcal{R}}^{\ast}\langle s_{i}\theta\sigma^{\prime},[\,]\rangle$ for all $i=1,\ldots,n$, and $s=t[l\theta\sigma^{\prime}]_{p}$. Note that $\theta\sigma^{\prime}=\sigma^{\prime}\theta=\theta\cup\sigma^{\prime}$ since $\mathsf{{{\mathcal{D}}}om}(\theta)\cap\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\varnothing$ and both substitutions are ground.

As in the unconditional case, we denote the union of both relations $\rightharpoonup_{\mathcal{R}}\cup\leftharpoondown_{\mathcal{R}}$ by $\rightleftharpoons_{\mathcal{R}}$.

Example 15

Consider again the DCTRS ${\mathcal{R}}$ from Example 1:

$$\begin{array}[]{l@{~}r@{~}c@{~}l@{}l@{~}r@{~}c@{~}l}\beta_{1}:\hfil~{}&\mathsf{add}(\mathsf{0},y)~{}&\to\hfil~{}&y&\beta_{4}:\hfil~{}&\mathsf{even}(\mathsf{0})~{}&\to\hfil~{}&\mathsf{true}\\ \beta_{2}:\hfil~{}&\mathsf{add}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\mathsf{s}(\mathsf{add}(x,y))&\beta_{5}:\hfil~{}&\mathsf{even}(\mathsf{s}(\mathsf{s}(x)))~{}&\to\hfil~{}&\mathsf{even}(x)\\ \beta_{3}:\hfil~{}&\mathsf{double}(x)~{}&\to\hfil~{}&\mathsf{add}(x,x)\Leftarrow\mathsf{even}(x)\twoheadrightarrow\mathsf{true}\\ \end{array}$$

Given the term $\mathsf{double}(\mathsf{s}(\mathsf{s}(\mathsf{0})))$, we have, for instance, the following forward derivation:

$$\begin{array}[]{lll}\langle\mathsf{double}(\mathsf{s}(\mathsf{s}(\mathsf{0}))),{[\,]}\rangle\\ \mbox{}\hskip 43.05542pt\rightharpoonup_{\mathcal{R}}~{}\langle\mathsf{add}(\mathsf{s}(\mathsf{s}(\mathsf{0})),\mathsf{s}(\mathsf{s}(\mathsf{0}))),{[\beta_{3}(\epsilon,id,{\pi})]}\rangle\\ \mbox{}\hskip 43.05542pt\rightharpoonup_{\mathcal{R}}~{}\cdots\\ \mbox{}\hskip 43.05542pt\rightharpoonup_{\mathcal{R}}~{}\langle\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{s}(\mathsf{0})))),{[\beta_{1}(1.1,id),\beta_{2}(1,id),\beta_{2}(\epsilon,id),\beta_{3}(\epsilon,id,{\pi})]}\rangle\\ \end{array}$$

where ${\pi}={[\beta_{4}(\epsilon,id),\beta_{5}(\epsilon,id)]}$ since we have the following reduction:

$$\langle\mathsf{even}(\mathsf{s}(\mathsf{s}(\mathsf{0}))),{[\,]}\rangle\rightharpoonup_{\mathcal{R}}\langle\mathsf{even}(\mathsf{0}),{[\beta_{5}(\epsilon,id)]}\rangle\rightharpoonup_{\mathcal{R}}\langle\mathsf{true},{[\beta_{4}(\epsilon,id),\beta_{5}(\epsilon,id)]}\rangle$$

The reader can easily construct the associated backward derivation:

$$\langle\mathsf{add}(\mathsf{s}(\mathsf{s}(\mathsf{0})),\mathsf{s}(\mathsf{s}(\mathsf{0}))),{[\beta_{1}(1.1,id),\beta_{2}(1,id),\ldots]}\rangle\leftharpoondown_{\mathcal{R}}^{\ast}\langle\mathsf{double}(\mathsf{s}(\mathsf{s}(\mathsf{0}))),{[\,]}\rangle$$

Let us now explain why we need to store $\sigma^{\prime}$ in a step of the form $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}\langle t,\beta(p,\sigma^{\prime},\overline{\pi_{n}}):\pi\rangle$. Given a DCTRS, for each rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}$, the following conditions hold:

• 3-CTRS: $\mathsf{{{\mathcal{V}}}ar}(r)\subseteq\mathsf{{{\mathcal{V}}}ar}(l,\overline{s_{n}},\overline{t_{n}})$.

• Determinism: for all $i=1,\ldots,n$, we have $\mathsf{{{\mathcal{V}}}ar}(s_{i})\subseteq\mathsf{{{\mathcal{V}}}ar}(l,\overline{t_{i-1}})$.

Intuitively, the backward relation $\leftharpoondown_{\mathcal{R}}$ can be seen as equivalent to the forward relation $\rightharpoonup_{\mathcal{R}}$ but using a reverse rule of the form $r\to l\Leftarrow t_{n}\twoheadrightarrow s_{n},\ldots,t_{1}\twoheadrightarrow s_{1}$. Therefore, in order to ensure that backward reduction is deterministic, we need the same conditions as above but on the reverse rule:

• 3-CTRS: $\mathsf{{{\mathcal{V}}}ar}(l)\subseteq\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}})$.

• Determinism: for all $i=1,\ldots,n$, $\mathsf{{{\mathcal{V}}}ar}(t_{i})\subseteq\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$.

Since these conditions cannot be guaranteed in general, we store

$$\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$$

in the trace term so that $(r\to l\Leftarrow t_{n}\twoheadrightarrow s_{n},\ldots,t_{1}\twoheadrightarrow s_{1})\sigma^{\prime}$ is deterministic and fulfills the conditions of a 3-CTRS by construction, i.e., $\mathsf{{{\mathcal{V}}}ar}(l\sigma^{\prime})\subseteq\mathsf{{{\mathcal{V}}}ar}(r\sigma^{\prime},\overline{s_{n}\sigma^{\prime}},\overline{t_{n}\sigma^{\prime}})$ and for all $i=1,\ldots,n$, $\mathsf{{{\mathcal{V}}}ar}(t_{i}\sigma^{\prime})\subseteq\mathsf{{{\mathcal{V}}}ar}(r\sigma^{\prime},\overline{s_{i+1,n}\sigma^{\prime}})$; see the proof of Theorem 21 for more details.

Example 16

Consider the following DCTRS:

$$\begin{array}[]{l}\beta_{1}:~{}\mathsf{f}(x,y,m)~{}\to~{}\mathsf{s}(w)\Leftarrow\mathsf{h}(x)\twoheadrightarrow x,\mathsf{g}(y,\mathsf{4})\twoheadrightarrow w\\ \beta_{2}:~{}\mathsf{h}(\mathsf{0})~{}\to~{}\mathsf{0}~{}~{}~{}~{}~{}~{}~{}~{}~{}\beta_{3}:~{}\mathsf{h}(\mathsf{1})~{}\to~{}\mathsf{1}~{}~{}~{}~{}~{}~{}~{}~{}~{}\beta_{4}:~{}\mathsf{g}(x,y)~{}\to~{}x\\ \end{array}$$

and the step $\langle\mathsf{f}(\mathsf{0},\mathsf{2},\mathsf{4}),[\,]\rangle\rightharpoonup_{\mathcal{R}}\langle\mathsf{s}(\mathsf{2}),[\beta_{1}(\epsilon,\sigma^{\prime},\pi_{1},\pi_{2})]\rangle$ with $\sigma^{\prime}=\{m\mapsto\mathsf{4},x\mapsto\mathsf{0}\}$, $\pi_{1}=[\beta_{2}(\epsilon,id)]$ and $\pi_{2}=[\beta_{4}(\epsilon,\{y\mapsto\mathsf{4}\})]$. The binding of variable $m$ is required to recover the value of the erased variable $m$, but the binding of variable $x$ is also needed to perform the subderivation $\langle x,\pi_{1}\rangle\leftharpoondown_{\mathcal{R}}\langle\mathsf{h}(x),[\,]\rangle$ when applying a backward step from $\langle\mathsf{s}(\mathsf{2}),[\beta_{1}(\epsilon,\sigma^{\prime},\pi_{1},\pi_{2})]\rangle$. If the binding for $x$ were unknown, this step would not be deterministic. As mentioned above, an instantiated reverse rule $(\mathsf{s}(w)\to\mathsf{f}(x,y,m)\Leftarrow w\twoheadrightarrow\mathsf{g}(y,\mathsf{4}),x\twoheadrightarrow\mathsf{h}(x))\sigma^{\prime}~{}=~{}\mathsf{s}(w)\to\mathsf{f}(\mathsf{0},y,\mathsf{4})\Leftarrow w\twoheadrightarrow\mathsf{g}(y,\mathsf{4}),\mathsf{0}\twoheadrightarrow\mathsf{h}(\mathsf{0})$ would be a legal DCTRS rule thanks to $\sigma^{\prime}$.

We note that similar conditions could be defined for arbitrary 3-CTRSs. However, the conditions would be much more involved; e.g., one had to compute first the variable dependencies between the equations in the conditions. Therefore, we prefer to keep the simpler conditions for DCTRSs (where these dependencies are fixed), which is still quite a general class of CTRSs.

Reversible rewriting is also a conservative extension of rewriting for DCTRSs (we omit the proof since it is straightforward):

Theorem 17

Let ${\mathcal{R}}$ be a DCTRS. Given ground terms $s,t$, if $s\to_{\mathcal{R}}^{\ast}t$, then for any trace $\pi$ there exists a trace $\pi^{\prime}$ such that $\langle s,\pi\rangle\rightharpoonup_{\mathcal{R}}^{\ast}\langle t,\pi^{\prime}\rangle$.

For the following result, we need some preliminary notions (see, e.g., [36]). For every oriented CTRS ${\mathcal{R}}$, we inductively define the TRSs ${\mathcal{R}}_{k}$, $k\geq 0$, as follows:

$$\begin{array}[]{l@{~}l@{~}l}{\mathcal{R}}_{0}\hfil~{}&=\hfil~{}&\varnothing\\ {\mathcal{R}}_{k+1}\hfil~{}&=\hfil~{}&\{l\sigma\to r\sigma\mid l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}},~{}s_{i}\sigma\to^{\ast}_{{\mathcal{R}}_{k}}t_{i}\sigma~{}\mbox{for all}~{}i=1,\ldots,n\}\end{array}$$

Observe that ${\mathcal{R}}_{k}\subseteq{\mathcal{R}}_{k+1}$ for all $k\geq 0$. We have $\to_{\mathcal{R}}=\bigcup_{i\geq 0}\to_{{\mathcal{R}}_{i}}$. We also have $s\to_{\mathcal{R}}t$ iff $s\to_{{\mathcal{R}}_{k}}t$ for some $k\geq 0$. The minimum such $k$ is called the depth of $s\to_{\mathcal{R}}t$, and the maximum depth $k$ of $s=s_{0}\to_{{\mathcal{R}}_{k_{1}}}\cdots\to_{{\mathcal{R}}_{k_{m}}}s_{m}=t$ (i.e., $k$ is the maximum of depths $k_{1},\ldots,k_{m}$) is called the depth of the derivation. If a derivation has depth $k$ and length $m$, we write $s\to_{{\mathcal{R}}_{k}}^{m}t$. Analogous notions can naturally be defined for $\rightharpoonup_{\mathcal{R}}$, $\leftharpoondown_{\mathcal{R}}$, and $\rightleftharpoons_{\mathcal{R}}$.

The next result shows that safe pairs are also preserved through reversible rewriting with DCTRSs:

Lemma 18

Let ${\mathcal{R}}$ be a DCTRS and $\langle s,\pi\rangle$ a safe pair. If $\langle s,\pi\rangle\rightleftharpoons_{\mathcal{R}}^{\ast}\langle t,\pi^{\prime}\rangle$, then $\langle t,\pi^{\prime}\rangle$ is also safe.

Proof 4

We prove the claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the derivation $\langle s,\pi\rangle\rightleftharpoons_{{\mathcal{R}}_{k}}^{m}\langle t,\pi^{\prime}\rangle$. Since the base case is trivial, we consider the inductive case $(k,m)>(0,0)$. Consider a derivation $\langle s,\pi\rangle\rightleftharpoons_{{\mathcal{R}}_{k}}^{m-1}\langle s_{0},\pi_{0}\rangle\rightleftharpoons_{{\mathcal{R}}_{k}}\langle t,\pi^{\prime}\rangle$. By the induction hypothesis, we have that $\langle s_{0},\pi_{0}\rangle$ is safe. Now, we distinguish two cases depending on the last step. If the last step is $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{{\mathcal{R}}_{k}}\langle t,\pi^{\prime}\rangle$, then there exist a position $p\in\mathsf{{{\cal P}}os}(s_{0})$, a rewrite rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s_{0}|_{p}=l\sigma$, $\langle s_{i}\sigma,[\,]\rangle\rightharpoonup_{{\mathcal{R}}_{k_{i}}}^{\ast}\langle t_{i}\sigma,\pi_{i}\rangle$ for all $i=1,\ldots,n$, $t=s_{0}[r\sigma]_{p}$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$, and $\pi^{\prime}=\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n})$. Then, since $k_{i}<k$, $i=1,\ldots,n$, $\sigma^{\prime}$ is ground and $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$ by construction, the claim follows by induction. Finally, if the last step has the form $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle t,\pi^{\prime}\rangle$, then the claim follows trivially since a step with $\leftharpoondown_{\mathcal{R}}$ only removes trace terms from $\pi_{0}$.

As in the unconditional case, the following proposition follows straightforwardly from the previous lemma since any pair with an empty trace is safe.

Proposition 19

Let ${\mathcal{R}}$ be a DCTRS. If $\langle s,[\,]\rangle\rightleftharpoons_{\mathcal{R}}^{\ast}\langle t,\pi\rangle$, then $\langle t,\pi\rangle$ is safe in ${\mathcal{R}}$.

Now, we can already state the reversibility of $\rightharpoonup_{\mathcal{R}}$ for DCTRSs:

Theorem 20

Let ${\mathcal{R}}$ be a DCTRS. Given the safe pairs $\langle s,\pi\rangle$ and $\langle t,\pi^{\prime}\rangle$, for all $k,m\geq 0$, $\langle s,\pi\rangle\rightharpoonup_{{\mathcal{R}}_{k}}^{m}\langle t,\pi^{\prime}\rangle$ iff $\langle t,\pi^{\prime}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}^{m}\langle s,\pi\rangle$.

Proof 5

$(\Rightarrow)$ We prove the claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the derivation $\langle s,\pi\rangle\rightharpoonup_{{\mathcal{R}}_{k}}^{m}\langle t,\pi^{\prime}\rangle$. Since the base case is trivial, we consider the inductive case $(k,m)>(0,0)$. Consider a derivation $\langle s,\pi\rangle\rightharpoonup_{{\mathcal{R}}_{k}}^{m-1}\langle s_{0},\pi_{0}\rangle\rightharpoonup_{{\mathcal{R}}_{k}}\langle t,\pi^{\prime}\rangle$ whose associated product is $(k,m)$. By Proposition 19, both $\langle s_{0},\pi_{0}\rangle$ and $\langle t,\pi^{\prime}\rangle$ are safe. By the induction hypothesis, since $(k,m-1)<(k,m)$, we have $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}^{m-1}\langle s,\pi\rangle$. Consider now the step $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{{\mathcal{R}}_{k}}\langle t,\pi^{\prime}\rangle$. Thus, there exist a position $p\in\mathsf{{{\cal P}}os}(s_{0})$, a rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a ground substitution $\sigma$ such that $s_{0}|_{p}=l\sigma$, $\langle s_{i}\sigma,[\,]\rangle\rightharpoonup_{{\mathcal{R}}_{k_{i}}}^{\ast}\langle t_{i}\sigma,\pi_{i}\rangle$ for all $i=1,\ldots,n$, $t=s_{0}[r\sigma]_{p}$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$, and $\pi^{\prime}=\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi_{0}$. By definition of $\rightharpoonup_{{\mathcal{R}}_{k}}$, we have that $k_{i}<k$ and, thus, $(k_{i},m_{1})<(k,m_{2})$ for all $i=1,\ldots,n$ and for all $m_{1},m_{2}$. Hence, by the induction hypothesis, we have $\langle t_{i}\sigma,\pi_{i}\rangle\leftharpoondown_{{\mathcal{R}}_{k_{i}}}^{\ast}\langle s_{i}\sigma,[\,]\rangle$ for all $i=1,\ldots,n$. Let $\theta=\sigma\!\mathrel{|\grave{}}_{\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}})\backslash\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})}$, so that $\sigma=\theta\sigma^{\prime}$ and $\mathsf{{{\mathcal{D}}}om}(\theta)\cap\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\varnothing$. Therefore, we have $\langle t,\pi^{\prime}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle s^{\prime}_{0},\pi_{0}\rangle$ with $t|_{p}=r\theta$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$ and $s^{\prime}_{0}=t[l\theta\sigma^{\prime}]_{p}=t[l\sigma]_{p}=s_{0}$, and the claim follows.

$(\Leftarrow)$ This direction proceeds in a similar way. We prove the claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the considered derivation. Since the base case is trivial, let us consider the inductive case $(k,m)>(0,0)$. Consider a derivation $\langle t,\pi^{\prime}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}^{m-1}\langle s_{0},\pi_{0}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle s,\pi\rangle$ whose associated product is $(k,m)$. By Proposition 19, both $\langle s_{0},\pi_{0}\rangle$ and $\langle s,\pi\rangle$ are safe. By the induction hypothesis, since $(k,m-1)<(k,m)$, we have $\langle s_{0},\pi_{0}\rangle\rightharpoonup_{{\mathcal{R}}_{k}}^{m-1}\langle t,\pi^{\prime}\rangle$. Consider now the step $\langle s_{0},\pi_{0}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle s,\pi\rangle$. Then, we have $\pi_{0}=\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and there exists a ground substitution $\theta$ with $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}})\backslash\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})$ such that $s_{0}|_{p}=r\theta$, $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle\leftharpoondown_{{\mathcal{R}}_{k_{i}}}^{\ast}\langle s_{i}\theta\sigma^{\prime},[\,]\rangle$ for all $i=1,\ldots,n$, and $s=s_{0}[l\theta\sigma^{\prime}]_{p}$. Moreover, since $\langle s_{0},\pi_{0}\rangle$ is safe, we have that $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$. By definition of $\leftharpoondown_{{\mathcal{R}}_{k}}$, we have that $k_{i}<k$ and, thus, $(k_{i},m_{1})<(k,m_{2})$ for all $i=1,\ldots,n$ and for all $m_{1},m_{2}$. By the induction hypothesis, we have $\langle s_{i}\theta\sigma^{\prime},[\,]\rangle\rightharpoonup_{{\mathcal{R}}_{k_{i}}}^{\ast}\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle$ for all $i=1,\ldots,n$. Let $\sigma=\theta\sigma^{\prime}$, with $\mathsf{{{\mathcal{D}}}om}(\theta)\cap\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=\varnothing$. Then, since $s|_{p}=l\sigma$, we can perform the step $\langle s,\pi\rangle\rightharpoonup_{{\mathcal{R}}_{k}}\langle s^{\prime}_{0},\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi\rangle$ with $s^{\prime}_{0}=s[r\sigma]_{p}=s[r\theta\sigma^{\prime}]_{p}$; moreover, $s[r\theta\sigma^{\prime}]_{p}=s[r\theta]_{p}=s_{0}[r\theta]_{p}=s_{0}$ since $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})\cap\mathsf{{{\mathcal{V}}}ar}(r)=\varnothing$, which concludes the proof.

In the following, we say that $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s,\pi\rangle$ is a deterministic step if there is no other, different pair $\langle s^{\prime\prime},\pi^{\prime\prime}\rangle$ with $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}\langle s^{\prime\prime},\pi^{\prime\prime}\rangle$ and, moreover, the subderivations for the equations in the condition of the applied rule (if any) are deterministic, too. We say that a derivation $\langle t,\pi^{\prime}\rangle\leftharpoondown_{\mathcal{R}}^{\ast}\langle s,\pi\rangle$ is deterministic if each reduction step in the derivation is deterministic.

Now, we can already prove that backward reversible rewriting is also deterministic, as in the unconditional case:

Theorem 21

Let ${\mathcal{R}}$ be a DCTRS. Let $\langle t,\pi^{\prime}\rangle$ be a safe pair with $\langle t,\pi^{\prime}\rangle\leftharpoondown^{\ast}_{\mathcal{R}}\langle s,\pi\rangle$ for some term $s$ and trace $\pi$. Then $\langle t,\pi^{\prime}\rangle\leftharpoondown^{\ast}_{\mathcal{R}}\langle s,\pi\rangle$ is deterministic.

Proof 6

We prove the claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the steps. The case $m=0$ is trivial, and thus we let $m>0$. Assume $\langle t,\pi^{\prime}\rangle\leftharpoondown^{m-1}_{{\mathcal{R}}_{k}}\langle u,\pi^{\prime\prime}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle s,\pi\rangle$. For the base case $k=1$, the applied rule is unconditional and the proof is analogous to that of Theorem 11.

Let us now consider $k>1$. By definition, if $\langle u,\pi^{\prime\prime}\rangle\leftharpoondown_{{\mathcal{R}}_{k}}\langle s,\pi\rangle$, we have $\pi^{\prime\prime}=\beta(p,\sigma^{\prime},\pi_{1},\ldots,\pi_{n}):\pi$, $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$ and there exists a ground substitution $\theta$ with $\mathsf{{{\mathcal{D}}}om}(\theta)=\mathsf{{{\mathcal{V}}}ar}(r)$ such that $u|_{p}=r\theta$, $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle\leftharpoondown_{{\mathcal{R}}_{j}}^{\ast}\langle s_{i}\theta\sigma^{\prime},[\,]\rangle$, $j<k$, for all $i=1,\ldots,n$, and $s=t[l\theta\sigma^{\prime}]_{p}$. By the induction hypothesis, the subderivations $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle\leftharpoondown_{{\mathcal{R}}_{j}}^{\ast}\langle s_{i}\theta\sigma^{\prime},[\,]\rangle$ are deterministic, i.e., $\langle s_{i}\theta\sigma^{\prime},[\,]\rangle$ is a unique resulting term obtained by reducing $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle$. Therefore, the only remaining source of nondeterminism can come from choosing a rule labeled with $\beta$ and from the computed substitution $\theta$. On the one hand, the labels are unique in ${\mathcal{R}}$. As for $\theta$, we prove that this is indeed the only possible substitution for the reduction step. Consider the instance of rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}$ with $\sigma^{\prime}$: $l\sigma^{\prime}\to r\sigma^{\prime}\Leftarrow\overline{s_{n}\sigma^{\prime}\twoheadrightarrow t_{n}\sigma^{\prime}}$. Since $\langle u,\pi^{\prime\prime}\rangle$ is safe, we have that $\sigma^{\prime}$ is a ground substitution and $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$. Then, the following properties hold:

• $\mathsf{{{\mathcal{V}}}ar}(l\sigma^{\prime})\subseteq\mathsf{{{\mathcal{V}}}ar}(r\sigma^{\prime},\overline{s_{n}\sigma^{\prime}},\overline{t_{n}\sigma^{\prime}})$, since $\sigma^{\prime}$ is ground and it covers all the variables in $\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}})$.

• $\mathsf{{{\mathcal{V}}}ar}(t_{i}\sigma^{\prime})\subseteq\mathsf{{{\mathcal{V}}}ar}(r\sigma^{\prime},\overline{s_{i+1,n}\sigma^{\prime}})$ for all $i=1,\ldots,n$, since $\sigma^{\prime}$ is ground and it covers all variables in $\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$.

The above properties guarantee that a rule of the form $r\sigma^{\prime}\to l\sigma^{\prime}\Leftarrow t_{n}\sigma^{\prime}\twoheadrightarrow s_{n}\sigma^{\prime},\ldots,t_{1}\sigma^{\prime}\twoheadrightarrow s_{1}\sigma^{\prime}$ can be seen as a rule of a DCTRS and, thus, there exists a deterministic procedure to compute $\theta$, which completes the proof.

Therefore, $\leftharpoondown_{\mathcal{R}}$ is deterministic and confluent. Termination is trivially guaranteed for pairs with a finite trace since the trace’s length strictly decreases with every backward step.

4 Removing Positions from Traces

Once we have a feasible definition of reversible rewriting, there are two refinements that can be considered: i) reducing the size of the traces and ii) defining a reversibilization transformation so that standard rewriting becomes reversible in the transformed system. In this section, we consider the first problem, leaving the second one for the next section.

In principle, one could remove information from the traces by requiring certain conditions on the considered systems. For instance, requiring injective functions may help to remove rule labels from trace terms. Also, requiring non-erasing rules may help to remove the second component of trace terms (i.e., the substitutions). In this section, however, we deal with a more challenging topic: removing positions from traces. This is useful not only to reduce the size of the traces but it is also essential to define a reversibilization technique for DCTRSs in the next section. In particular, we aim at transforming a given DCTRS into one that fulfills some conditions that make storing positions unnecessary.

In the following, given a CTRS ${\mathcal{R}}$, we say that a term $t$ is basic [18] if it has the form $f(\overline{t_{n}})$ with $f\in{\mathcal{D}}_{\mathcal{R}}$ a defined function symbol and $\overline{t_{n}}\in{\mathcal{T}}({\mathcal{C}}_{\mathcal{R}},{\mathcal{V}})$ constructor terms. Furthermore, in the remainder of this paper, we assume that the right-hand sides of the equations in the conditions of the rules of a DCTRS are constructor terms. This is not a significant restriction since these terms cannot be reduced anyway (since we consider oriented equations in this paper), and still covers most practical examples.

Now, we introduce the following subclass of DCTRSs:

Definition 22 (pcDCTRS [30])

We say that a DCTRS ${\mathcal{R}}$ is a pcDCTRS (“pc” stands for pure constructor) if, for each rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, we have that $l$ and $\overline{s_{n}}$ are basic terms and $r$ and $\overline{t_{n}}$ are constructor terms.

Pure constructor systems are called normalized systems in [3]. Also, they are mostly equivalent to the class III_n of conditional systems in [8], where $t_{1},\ldots,t_{n}$ are required to be ground unconditional normal forms instead.

In principle, any DCTRS with basic terms in the left-hand sides (i.e., a constructor DCTRS) and constructor terms in the right-hand sides of the equations of the rules can be transformed into a pcDCTRS by applying a few simple transformations: flattening and simplification of constructor conditions. Let us now consider each of these transformations separately. Roughly speaking, flattening involves transforming a term (occurring, e.g., in the right-hand side of a DCTRS or in the condition) with nested defined functions like $\mathsf{f}(\mathsf{g}(x))$ into a term $\mathsf{f}(y)$ and an (oriented) equation $\mathsf{g}(x)\twoheadrightarrow y$, where $y$ is a fresh variable. Formally,

Definition 23 (flattening)

Let ${\mathcal{R}}$ be a CTRS, $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})\in{\mathcal{R}}$ be a rule and $R^{\prime}$ be a new rule either of the form $l\to r\Leftarrow s_{1}\twoheadrightarrow t_{1},\ldots,s_{i}|_{p}\twoheadrightarrow w,s_{i}[w]_{p}\twoheadrightarrow t_{i},\ldots,s_{n}\twoheadrightarrow t_{n}$, for some $p\in\mathsf{{{\cal P}}os}(s_{i})$, $1\leqslant i\leqslant n$, or $l\to r[w]_{q}\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}},r|_{q}\twoheadrightarrow w$, for some $q\in\mathsf{{{\cal P}}os}(r)$, where $w$ is a fresh variable. Then, a CTRS ${\mathcal{R}}^{\prime}$ is obtained from ${\mathcal{R}}$ by a flattening step if ${\mathcal{R}}^{\prime}=({\mathcal{R}}\backslash\{R\})\cup\{R^{\prime}\}$.

Note that, if an unconditional rule is non-erasing (i.e., $\mathsf{{{\mathcal{V}}}ar}(l)\subseteq\mathsf{{{\mathcal{V}}}ar}(r)$ for a rule $l\to r$), any conditional rule obtained by flattening is trivially non-erasing too, according to the notion of non-erasingness for DCTRSs in [32].

Flattening is trivially complete since any flattening step can be undone by binding the fresh variable again to the selected subterm and, then, proceeding as in the original system. Soundness is more subtle though. In this work, we prove the correctness of flattening for arbitrary DCTRSs with respect to innermost rewriting. As usual, the innermost rewrite relation, in symbols, $\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\mathcal{R}}$, is defined as the smallest binary relation satisfying the following: given ground terms $s,t\in{\mathcal{T}}({\mathcal{F}})$, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\mathcal{R}}t$ iff there exist a position $p$ in $s$ such that no proper subterms of $s|_{p}$ are reducible, a rewrite rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a normalized ground substitution $\sigma$ such that $s|_{p}=l\sigma$, $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t_{i}\sigma$, for all $i=1,\ldots,n$, and $t=s[r\sigma]_{p}$.

In order to prove the correctness of flattening, we state the following auxiliary lemma:

Lemma 24

Let ${\mathcal{R}}$ be a DCTRS. Given terms $s$ and $t$, with $t$ a normal form, and a position $p\in\mathsf{{{\cal P}}os}(s)$, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s|_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>w\sigma$ and $s[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$, for some fresh variable $w$ and normalized substitution $\sigma$.

Proof 7

$(\Rightarrow)$ Let us consider an arbitrary position $p\in\mathsf{{{\cal P}}os}(s)$. If $s|_{p}$ is normalized, the proof is straightforward. Otherwise, since we use innermost reduction (leftmost innermost, for simplicity), we can represent the derivation $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ as follows:

$$s[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s^{\prime\prime}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$$

where $s^{\prime\prime}$ is a normal form and the subderivation $s[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s|_{p}]_{p}$ reduces the leftmost innermost subterms that are to the left of $s|_{p}$ (if any). Then, by choosing $\sigma=\{w\mapsto s^{\prime\prime}\}$ we have $s|_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>w\sigma$ (by mimicking the steps of $s^{\prime}[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s^{\prime\prime}]_{p}$), $s[w\sigma]_{p}{\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}}\>s^{\prime}[w\sigma]_{p}$ (by mimicking the steps of $s[s|_{p}]_{p}{\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}}\>s^{\prime}[s|_{p}]_{p}$), and $s^{\prime}[w\sigma]_{p}{\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}}\>t$ (by mimicking the steps of $s^{\prime}[s^{\prime\prime}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$), which concludes the proof.

$(\Leftarrow)$ This direction is perfectly analogous to the previous case. We consider an arbitrary position $p\in\mathsf{{{\cal P}}os}(s)$ such that $s|_{p}$ is not normalized (otherwise, the proof is trivial). Now, since derivations are innermost, we can consider that $s[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ is as follows: $s[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$, where $s[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[w\sigma]_{p}$ reduces the innermost subterms to the left of $s|_{p}$. Therefore, we have $s[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s|_{p}]_{p}$ (by mimicking the steps of $s[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[w\sigma]_{p}$), $s^{\prime}[s|_{p}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>s^{\prime}[s^{\prime\prime}]_{p}$ (by mimicking the steps of $s|_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>w\sigma$, with $\sigma=\{w\mapsto s^{\prime\prime}\}$), and $s^{\prime}[s^{\prime\prime}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ (by mimicking the steps of $s^{\prime}[w\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$).

The following theorem is an easy consequence of the previous lemma:

Theorem 25

Let ${\mathcal{R}}$ be a DCTRS. If ${\mathcal{R}}^{\prime}$ is obtained from ${\mathcal{R}}$ by a flattening step, then ${\mathcal{R}}^{\prime}$ is a DCTRS and, for all ground terms $s,t$, with $t$ a normal form, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$.

Proof 8

$(\Rightarrow)$ We prove the claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the derivation $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k}}\>t$. Since the base case is trivial, we consider the inductive case $(k,m)>(0,0)$. Assume that $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k}}\>t$ has the form $s[l\sigma]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{{\mathcal{R}}_{k}}\>s[r\sigma]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k}}\>t$ with $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$ and $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k_{i}}}\;t_{i}\sigma$, $k_{i}<k$, $i=1,\ldots,n$. If $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}^{\prime}$, the claim follows directly by induction. Otherwise, we have that either $l\to r\Leftarrow s_{1}\twoheadrightarrow t_{1},\ldots,s_{i}|_{p}\twoheadrightarrow w,s_{i}[w]_{p}\twoheadrightarrow t_{i},\ldots,s_{n}\twoheadrightarrow t_{n}\in{\mathcal{R}}^{\prime}$, for some $p\in\mathsf{{{\cal P}}os}(s_{i})$, $1\leqslant i\leqslant n$, or $l\to r[w]_{q}\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}},r|_{q}\twoheadrightarrow w\in{\mathcal{R}}^{\prime}$, for some $q\in\mathsf{{{\cal P}}os}(r)$, where $w$ is a fresh variable. Consider first the case $l\to r\Leftarrow s_{1}\twoheadrightarrow t_{1},\ldots,s_{i}|_{p}\twoheadrightarrow w,s_{i}[w]_{p}\twoheadrightarrow t_{i},\ldots,s_{n}\twoheadrightarrow t_{n}\in{\mathcal{R}}^{\prime}$, for some $p\in\mathsf{{{\cal P}}os}(s_{i})$, $1\leqslant i\leqslant n$. Since $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k_{i}}}\;t_{i}\sigma$, $k_{i}<k$, $i=1,\ldots,n$, by the induction hypothesis, we have $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\;t_{i}\sigma$, $i=1,\ldots,n$. By Lemma 24, there exists $\sigma^{\prime}=\{w\mapsto s^{\prime}\}$ for some normal form $s^{\prime}$ such that $s_{i}|_{p}\sigma=s_{i}|_{p}\sigma\sigma^{\prime}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k_{i}}}\>w\sigma\sigma^{\prime}=w\sigma^{\prime}$ and $s_{i}[w]_{p}\sigma\sigma^{\prime}=s_{i}\sigma[w\sigma^{\prime}]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k_{i}}}t_{i}$. Moreover, since $w$ is an extra variable, we also have $s_{j}\sigma\sigma^{\prime}=s_{j}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t_{j}\sigma=t_{j}\sigma\sigma^{\prime}$ for $j=1,\ldots,i-1,i+1,\ldots,n$. Therefore, since $l\sigma\sigma^{\prime}=l\sigma$ and $r\sigma\sigma^{\prime}=r\sigma$, we have $s[l\sigma]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{{\mathcal{R}}}s[r\sigma]_{u}$, and the claim follows by induction. Consider the second case. By the induction hypothesis, we have $s[r\sigma]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$ and $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t_{i}\sigma$ for all $i=1,\ldots,n$. By Lemma 24, there exists a substitution $\sigma^{\prime}=\{w\mapsto s^{\prime}\}$ such that $s^{\prime}$ is the normal form of $r|_{q}\sigma$ and we have $r|_{q}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>w\sigma^{\prime}$ and $s[r\sigma[w\sigma^{\prime}]_{q}]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$. Moreover, since $w$ is a fresh variable, we have $s_{i}\sigma\sigma^{\prime}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t_{i}\sigma\sigma^{\prime}$ for all $i=1,\ldots,n$. Therefore, we have $s[l\sigma\sigma^{\prime}]_{u}=s[l\sigma]_{u}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{{\mathcal{R}}^{\prime}}s[r\sigma[w\sigma^{\prime}]_{q}]_{u}$, which concludes the proof.

$(\Leftarrow)$ This direction is perfectly analogous to the previous one, and follows easily by Lemma 24 too.

Let us now consider the second kind of transformations: the simplification of constructor conditions. Basically, we can drop an equation $s\twoheadrightarrow t$ when the terms $s$ and $t$ are constructor, called a constructor condition, by either applying the most general unifier (mgu) of $s$ and $t$ (if it exists) to the remaining part of the rule, or by deleting entirely the rule if they do not unify because (under innermost rewriting) the equation will never be satisfied by any normalized substitution. Similar transformations can be found in [33].

In order to justify these transformations, we state and prove the following results. In the following, we let $mgu(s,t)$ denote the most general unifier of terms $s$ and $t$ if it exists, and $\mathit{fail}$ otherwise.

Theorem 26 (removal of unifiable constructor conditions)

Let ${\mathcal{R}}$ be a DCTRS and let $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})\in{\mathcal{R}}$ be a rule with $mgu(s_{i},t_{i})=\theta$, for some $i\in\{1,\ldots,n\}$, where $s_{i}$ and $t_{i}$ are constructor terms. Let $R^{\prime}$ be a new rule of the form $l\theta\to r\theta\Leftarrow s_{1}\theta\twoheadrightarrow t_{1}\theta,\ldots,s_{i-1}\theta\twoheadrightarrow t_{i-1}\theta,s_{i+1}\theta\twoheadrightarrow t_{i+1}\theta,\ldots,s_{n}\theta\twoheadrightarrow t_{n}\theta$. Then ${\mathcal{R}}^{\prime}=({\mathcal{R}}\backslash\{R\})\cup\{R^{\prime}\}$ is a DCTRS and, for all ground terms $s$ and $t$, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$.

Proof 9

$(\Rightarrow)$ First, we prove the following claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the steps: if $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{m}_{{\mathcal{R}}_{k}}\>t$, then $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$. It suffices to consider the case where $R$ is applied, i.e., $s=s[l\sigma]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\{R\}}\>s[r\sigma]_{p}$ with $s_{j}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}_{k_{j}}}\>t_{j}\sigma$ for all $j\in\{1,\ldots,n\}$. By definition, $\sigma$ is normalized. Hence, since $s_{i}$ and $t_{i}$ are constructor terms, we have that $s_{i}\sigma$ and $t_{i}\sigma$ are trivially normal forms since the normalized subterms introduced by $\sigma$ cannot become reducible in a constructor context. Therefore, we have $s_{i}\sigma=t_{i}\sigma$. Thus, $\sigma$ is a unifier of $s_{i}$ and $t_{i}$ and, hence, $\theta$ is more general than $\sigma$. Let $\delta$ be a substitution such that $\sigma=\theta\delta$. Since $\sigma$ is normalized, so is $\delta$. Since $k_{j}<k$ for all $j=1,\ldots,n$, by the induction hypothesis, we have that $s_{j}\sigma=s_{j}\theta\delta\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t_{j}\theta\delta=t_{j}\sigma$ for $j\in\{1,\ldots,i-1,i+1,\ldots,n\}$. Therefore, we have that $s[l\sigma]_{p}=s[l\theta\delta]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\{R^{\prime}\}}\>s[r\theta\delta]_{p}=s[r\sigma]_{p}$.

$(\Leftarrow)$ Now, we prove the following claim by induction on the lexicographic product $(k,m)$ of the depth $k$ and the length $m$ of the steps: if $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{m}_{{\mathcal{R}}^{\prime}_{k}}\>t$, then $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$. It suffices to consider the case where $R^{\prime}$ is applied, i.e., $s=s[l\theta\delta]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\{R\}}\>s[r\theta\delta]_{p}$ with $s_{j}\theta\delta\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}_{k_{j}}}\>t_{j}\theta\delta$ for all $j\in\{1,\ldots,i-1,i+1,\ldots,n\}$. By the assumption and the definition, $\theta$ and $\delta$ are normalized, and thus, $s_{i}\theta\delta$ and $t_{i}\theta\delta$ are normal forms (as in the previous case, because the normalized subterms introduced by $\theta\delta$ cannot become reducible in a constructor context), i.e., $s_{i}\theta\delta=t_{i}\theta\delta$. Since $k_{j}<k$ for all $j\in\{1,\ldots,i-1,i+1,\ldots,n\}$, by the induction hypothesis, we have that $s_{j}\theta\delta\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}}\>t_{j}\theta\delta$ for $j\in\{1,\ldots,i-1,i+1,\ldots,n\}$. Therefore, we have that $s[l\sigma]_{p}=s[l\theta\delta]_{p}\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\{R\}}\>s[r\theta\delta]_{p}=s[r\sigma]$ with $\sigma=\theta\delta$.

Now we consider the case when the terms in the constructor condition do not unify:

Theorem 27 (removal of infeasible rules)

Let ${\mathcal{R}}$ be a DCTRS and let $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})\in{\mathcal{R}}$ be a rule with $mgu(s_{i},t_{i})=\mathit{fail}$, for some $i\in\{1,\ldots,n\}$. Then ${\mathcal{R}}^{\prime}={\mathcal{R}}\backslash\{R\}$ is a DCTRS and, for all ground terms $s$ and $t$, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$.

Proof 10

Since ${\mathcal{R}}\supseteq{\mathcal{R}}^{\prime}$, the if part is trivial, and thus, we consider the only-if part. To apply $R$ to a term, there must exist a normalized substitution $\sigma$ such that $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t_{i}\sigma$. Since $s_{i},t_{i}$ are constructor terms and $\sigma$ is normalized, $s_{i}\sigma$ is a normal form (because the normalized subterms introduced by $\sigma$ cannot become reducible in a constructor context). If $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t_{i}\sigma$ is satisfied (i.e., $s_{i}\sigma=t_{i}\sigma$), then $s_{i}$ and $t_{i}$ are unifiable, and thus, this contradicts the assumption. Therefore, $R$ is never applied to any term, and hence, $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$.

Using flattening and the simplification of constructor conditions, any constructor DCTRS with constructor terms in the right-hand sides of the equations of the rules can be transformed into a pcDCTRS. One can use, for instance, the following simple algorithm. Let ${\mathcal{R}}$ be such a constructor DCTRS. We apply the following transformations as much as possible:

(flattening-rhs)

Assume that ${\mathcal{R}}$ contains a rule of the form $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})$ where $r$ is not a constructor term. Let $r|_{q}$, $q\in\mathsf{{{\cal P}}os}(r)$, be a basic subterm of $r$. Then, we replace rule $R$ by a new rule of the form $l\to r[w]_{q}\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}},r|_{q}\twoheadrightarrow w$, where $w$ is a fresh variable.

(flattening-condition)

Assume that ${\mathcal{R}}$ contains a rule of the form $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})$ where $s_{i}$ is neither a constructor term nor a basic term, $i\in\{1,\ldots,n\}$. Let $s_{i}|_{q}$, $q\in\mathsf{{{\cal P}}os}(s_{1})$, be a basic subterm of $s_{i}$. Then, we replace rule $R$ by a new rule of the form $l\to r\Leftarrow s_{1}\twoheadrightarrow t_{1},\ldots,s_{i}|_{q}\twoheadrightarrow w,s_{i}[w]_{q}\twoheadrightarrow t_{i},\ldots,s_{n}\twoheadrightarrow t_{n}$, where $w$ is a fresh variable.

(removal-unify)

Assume that ${\mathcal{R}}$ contains a rule of the form $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})$ where $s_{i}$ is a constructor term, $i\in\{1,\ldots,n\}$. If $mgu(s_{i},t_{i})=\theta\neq\mathit{fail}$, then we replace rule $R$ by a new rule of the form $l\theta\to r\theta\Leftarrow s_{1}\theta\twoheadrightarrow t_{1}\theta,\ldots,s_{i-1}\theta\twoheadrightarrow t_{i-1}\theta,s_{i+1}\theta\twoheadrightarrow t_{i+1}\theta,\ldots,s_{n}\theta\twoheadrightarrow t_{n}\theta$.

(removal-fail)

Assume that ${\mathcal{R}}$ contains a rule of the form $R=(l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}})$ where $s_{i}$ is a constructor term, $i\in\{1,\ldots,n\}$. If $mgu(s_{i},t_{i})=\mathit{fail}$, then we remove rule $R$ from ${\mathcal{R}}$.

Trivially, by applying rule flattening-rhs as much as possible, we end up with a DCTRS where all the right-hand sides are constructor terms; analogously, the exhaustive application of rule flattening-condition allows us to ensure that the left-hand sides of all equations in the conditions of the rules are either constructor or basic; finally, the application of rules removal-unify and removal-fail produces a pcDCTRS by removing those equations in which the left-hand side is a constructor term. Therefore, in the remainder of this paper, we only consider pcDCTRSs.

A nice property of pcDCTRSs is that one can consider reductions only at topmost positions. Formally, given a pcDCTRS ${\mathcal{R}}$, we say that $s\to_{p,l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}}t$ is a top reduction step if $p=\epsilon$, there is a ground substitution $\sigma$ with $s=l\sigma$, $s_{i}\sigma\to^{\ast}_{\mathcal{R}}t_{i}\sigma$ for all $i=1,\ldots,n$, $t=r\sigma$, and all the steps in $s_{i}\sigma\to^{\ast}_{\mathcal{R}}t_{i}\sigma$ for $i=1,\ldots,n$ are also top reduction steps. We denote top reductions with $\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}$ for standard rewriting, and $\stackrel{{\scriptstyle\epsilon}}{{\rightharpoonup}}_{\mathcal{R}},\stackrel{{\scriptstyle\epsilon}}{{\leftharpoondown}}_{\mathcal{R}}$ for our reversible rewrite relations.

The following result basically states that $\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}$ and $\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}$ are equivalent for pcDCTRSs:

Theorem 28

Let ${\mathcal{R}}$ be a constructor DCTRS with constructor terms in the right-hand sides of the equations and ${\mathcal{R}}^{\prime}$ be a pcDCTRS obtained from ${\mathcal{R}}$ by a sequence of transformations of flattening and simplification of constructor conditions. Given ground terms $s$ and $t$ such that $s$ is basic and $t$ is normalized, we have $s\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t$ iff $s\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}\!\!{}^{\ast}_{{\mathcal{R}}^{\prime}}\>t$.

Proof 11

First, it is straightforward to see that an innermost reduction in ${\mathcal{R}}^{\prime}$ can only reduce the topmost positions of terms since defined functions can only occur at the root of terms and the terms introduced by instantiation are, by definition, irreducible. Therefore, the claim is a consequence of Theorems 25, 26 and 27, together with the above fact.

Therefore, when considering pcDCTRSs and top reductions, storing the reduced positions in the trace terms becomes redundant since they are always $\epsilon$. Thus, in practice, one can consider simpler trace terms without positions, $\beta(\sigma,\pi_{1},\ldots,\pi_{n})$, that implicitly represent the trace term $\beta(\epsilon,\sigma,\pi_{1},\ldots,\pi_{n})$.

Example 29

Consider the following TRS ${\mathcal{R}}$ defining addition and multiplication on natural numbers, and its associated pcDCTRS ${\mathcal{R}}^{\prime}$:

$$\begin{array}[]{l@{}r@{~}c@{~}l@{}l@{~}r@{~}c@{~}l}{\mathcal{R}}=\{&\mathsf{add}(\mathsf{0},y)~{}&\to\hfil~{}&y,\\ &\mathsf{add}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\mathsf{s}(\mathsf{add}(x,y)),\\ &\mathsf{mult}(\mathsf{0},y)~{}&\to\hfil~{}&\mathsf{0},\\ &\mathsf{mult}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\mathsf{add}(\mathsf{mult}(x,y),y)&\}\hfil~{}\end{array}$$

$$\begin{array}[]{l@{}r@{~}c@{~}l@{}l@{~}r@{~}c@{~}l}{\mathcal{R}}^{\prime}=\{&\mathsf{add}(\mathsf{0},y)~{}&\to\hfil~{}&y,\\ &\mathsf{add}(\mathsf{s}(x),y)~{}&\to\hfil~{}&\mathsf{s}(z)\Leftarrow\mathsf{add}(x,y)\twoheadrightarrow z,\\ &\mathsf{mult}(\mathsf{0},y)~{}&\to\hfil~{}&\mathsf{0},\\ &\mathsf{mult}(\mathsf{s}(x),y)~{}&\to\hfil~{}&w\Leftarrow\mathsf{mult}(x,y)\twoheadrightarrow z,\mathsf{add}(z,y)\twoheadrightarrow w&\}\hfil~{}\\ \end{array}$$

For instance, given the following reduction in ${\mathcal{R}}$:

$$\mathsf{mult}(\mathsf{s}(\mathsf{0}),\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\mathcal{R}}\mathsf{add}(\mathsf{mult}(\mathsf{0},\mathsf{s}(\mathsf{0})),\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\mathcal{R}}\mathsf{add}(\mathsf{0},\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{i}}}{{\rightarrow}}_{\mathcal{R}}\mathsf{s}(\mathsf{0})$$

we have the following counterpart in ${\mathcal{R}}^{\prime}$:

$$\begin{array}[]{lr@{~}l}\mathsf{mult}(\mathsf{s}(\mathsf{0}),\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}^{\prime}}\mathsf{s}(\mathsf{0})&\mbox{with}~{}&\mathsf{mult}(\mathsf{0},\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}^{\prime}}\mathsf{0}\\ &\mbox{and}~{}&\mathsf{add}(\mathsf{0},\mathsf{s}(\mathsf{0}))\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}^{\prime}}\mathsf{s}(\mathsf{0})\end{array}$$

Trivially, all results in Section 3 hold for pcDCTRSs and top reductions starting from basic terms. The simpler trace terms without positions will allow us to introduce appropriate injectivization and inversion transformations in the next section.

5 Reversibilization

In this section, we aim at compiling the reversible extension of rewriting into the system rules. Intuitively speaking, given a pure constructor system ${\mathcal{R}}$, we aim at producing new systems ${\mathcal{R}}_{f}$ and ${\mathcal{R}}_{b}$ such that standard rewriting in ${\mathcal{R}}_{f}$, i.e., $\to_{{\mathcal{R}}_{f}}$, coincides with the forward reversible extension $\rightharpoonup_{\mathcal{R}}$ in the original system, and analogously $\to_{{\mathcal{R}}_{b}}$ is equivalent to $\leftharpoondown_{\mathcal{R}}$. Therefore, ${\mathcal{R}}_{f}$ can be seen as an injectivization of ${\mathcal{R}}$, and ${\mathcal{R}}_{b}$ as the inversion of ${\mathcal{R}}_{f}$.

In principle, we could easily introduce a transformation for pcDCTRSs that mimicks the behavior of the reversible extension of rewriting. For instance, given the pcDCTRS ${\mathcal{R}}$ of Example 16, we could produce the following injectivized version ${\mathcal{R}}_{f}$:

$$\begin{array}[]{@{}r@{~}c@{~}l@{~}l}\langle\mathsf{f}(x,y,m),ws\rangle~{}&\to\hfil~{}&\langle\mathsf{s}(w),\beta_{1}(m,x,w_{1},w_{2}):ws\rangle\hfil~{}\\ ~{}&\hfil~{}&\mbox{}\hskip 8.61108pt\Leftarrow\langle\mathsf{h}(x),[\,]\rangle\twoheadrightarrow\langle x,w_{1}\rangle,\langle\mathsf{g}(y,\mathsf{4}),[\,]\rangle\twoheadrightarrow\langle w,w_{2}\rangle\hfil~{}\\ \langle\mathsf{h}(\mathsf{0}),ws\rangle~{}&\to\hfil~{}&\langle\mathsf{0},\beta_{2}:ws\rangle\hfil~{}\\ \langle\mathsf{h}(\mathsf{1}),ws\rangle~{}&\to\hfil~{}&\langle\mathsf{1},\beta_{3}:ws\rangle\hfil~{}\\ \langle\mathsf{g}(x,y),ws\rangle~{}&\to\hfil~{}&\langle x,\beta_{4}(y):ws\rangle\hfil~{}\\ \end{array}$$

For instance, the reversible step $\langle\mathsf{f}(\mathsf{0},\mathsf{2},\mathsf{4}),[\,]\rangle\stackrel{{\scriptstyle\epsilon}}{{\rightharpoonup}}_{\mathcal{R}}\langle\mathsf{s}(\mathsf{2}),[\beta_{1}(\sigma^{\prime},\pi_{1},\pi_{2})]\rangle$ with $\sigma^{\prime}=\{m\mapsto\mathsf{4},x\mapsto\mathsf{0}\}$, $\pi_{1}=[\beta_{2}(id)]$ and $\pi_{2}=[\beta_{4}(\{y\mapsto\textsf{4}\})]$, has the following counterpart in ${\mathcal{R}}_{f}$:

$$\begin{array}[]{lll}\langle\mathsf{f}(\mathsf{0},\mathsf{2},\mathsf{4}),[\,]\rangle\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\langle\mathsf{s}(\mathsf{2}),[\beta_{1}(\mathsf{4},\mathsf{0},[\beta_{2}],[\beta_{4}(\mathsf{4})])]\rangle\\ \mbox{}\hskip 43.05542pt\mbox{with}~{}~{}\langle\mathsf{h}(\mathsf{0}),[\,]\rangle\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\langle\mathsf{0},[\beta_{2}]\rangle~{}~{}\mbox{and}~{}~{}\langle\mathsf{g}(\mathsf{2},\mathsf{4}),[\,]\rangle\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\langle\mathsf{2},[\beta_{4}(\mathsf{4})]\rangle\\ \end{array}$$

The only subtle difference here is that a trace term like

$$\beta_{1}(\{m\mapsto\mathsf{4},x\mapsto\mathsf{0}\},[\beta_{2}(id)],[\beta_{4}(\{y\mapsto\textsf{4}\})])$$

is now stored in the transformed system as

$$\beta_{1}(\mathsf{4},\mathsf{0},[\beta_{2}],[\beta_{4}(\mathsf{4})])$$

Furthermore, we could produce an inverse ${\mathcal{R}}_{b}$ of the above system as follows:

$$\begin{array}[]{r@{~}c@{~}l@{~}l}\langle\mathsf{s}(w),\beta_{1}(m,x,w_{1},w_{2}):ws\rangle^{-1}~{}&\to\hfil~{}&\langle\mathsf{f}(x,y,m),ws\rangle^{-1}\hfil~{}\\ ~{}&\hfil~{}&\mbox{}\hskip 8.61108pt\Leftarrow\langle w,w_{2}\rangle^{-1}\twoheadrightarrow\langle\mathsf{g}(y,\mathsf{4}),[\,]\rangle^{-1},\hfil~{}\\ ~{}&\hfil~{}&\mbox{}\hskip 23.68048pt\langle x,w_{1}\rangle^{-1}\twoheadrightarrow\langle\mathsf{h}(x),[\,]\rangle^{-1}\hfil~{}\\ \langle\mathsf{0},\beta_{2}:ws\rangle^{-1}~{}&\to\hfil~{}&\langle\mathsf{h}(\mathsf{0}),ws\rangle^{-1}\hfil~{}\\ \langle\mathsf{1},\beta_{3}:ws\rangle^{-1}~{}&\to\hfil~{}&\langle\mathsf{h}(\mathsf{1}),ws\rangle^{-1}\hfil~{}\\ \langle x,\beta_{4}(y):ws\rangle^{-1}~{}&\to\hfil~{}&\langle\mathsf{g}(x,y),ws\rangle^{-1}\hfil~{}\\ \end{array}$$

mainly by switching the left- and right-hand sides of each rule and condition. The correctness of these injectivization and inversion transformations would be straightforward.

These transformations are only aimed at mimicking, step by step, the reversible relations $\rightharpoonup_{{\mathcal{R}}}$ and $\leftharpoondown_{{\mathcal{R}}}$. Roughly speaking, for each step $\langle s,\pi\rangle\rightharpoonup_{{\mathcal{R}}}\langle t,\pi^{\prime}\rangle$ in a system ${\mathcal{R}}$, we have $\langle s,\pi\rangle\to_{{\mathcal{R}}_{f}}\langle t,\pi^{\prime}\rangle$, where ${\mathcal{R}}_{f}$ is the injectivized version of ${\mathcal{R}}$, and for each step $\langle s,\pi\rangle\leftharpoondown_{{\mathcal{R}}}\langle t,\pi^{\prime}\rangle$ in ${\mathcal{R}}$, we have $\langle s,\pi\rangle\to_{{\mathcal{R}}_{b}}\langle t,\pi^{\prime}\rangle$, where ${\mathcal{R}}_{b}$ is the inverse of ${\mathcal{R}}_{f}$. More details on this approach can be found in [31]. Unfortunately, it might be much more useful to produce injective and inverse versions of each function defined in a system ${\mathcal{R}}$. Note that, in the above approach, the system ${\mathcal{R}}_{f}$ only defines a single function $\langle\_,\_\rangle$ and ${\mathcal{R}}_{b}$ only defines $\langle\_,\_\rangle^{-1}$, i.e., we are computing systems that define the relations $\rightharpoonup_{\mathcal{R}}$ and $\leftharpoondown_{\mathcal{R}}$ rather than the injectivized and inverse versions of the functions in ${\mathcal{R}}$. In the following, we introduce more refined transformations that can actually produce injective and inverse versions of the original functions.

5.1 Injectivization

In principle, given a function $\mathsf{f}$, one can consider that the injectivization of a rule of the form

$$\beta:\mathsf{f}(\overline{s_{0}})\to r\Leftarrow\mathsf{f_{1}}(\overline{s_{1}})\twoheadrightarrow t_{1},\ldots,\mathsf{f_{n}}(\overline{s_{n}})\twoheadrightarrow t_{n}$$

produces the following rule

$$\mathsf{f}^{\mathtt{i}}(\overline{s_{0}})\to\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\Leftarrow\mathsf{f}_{1}^{\mathtt{i}}(\overline{s_{1}})\twoheadrightarrow\langle t_{1},w_{1}\rangle\ldots,\mathsf{f}_{n}^{\mathtt{i}}(\overline{s_{n}})\twoheadrightarrow\langle t_{n},w_{n}\rangle$$

where $\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$ and $\overline{w_{n}}$ are fresh variables. The following example, though, illustrates that this is not correct in general.

Example 30

Consider the following pcDCTRS ${\mathcal{R}}$:

$$\begin{array}[]{lrcl}\beta_{1}:&\mathsf{f}(x,y)&\to&z\Leftarrow\mathsf{h}(y)\twoheadrightarrow w,~{}\mathsf{first}(x,w)\twoheadrightarrow z\\ \beta_{2}:&\mathsf{h}(\mathsf{0})&\to&\mathsf{0}\\ \beta_{3}:&\mathsf{first}(x,y)&\to&x\\ \end{array}$$

together with the following top reduction:

$$\begin{array}[]{@{}ll@{}}\mathsf{f}(\mathsf{2},\mathsf{1})\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{\mathcal{R}}\mathsf{2}&\mbox{with}~{}\sigma=\{x\mapsto\mathsf{2},y\mapsto\mathsf{1},w\mapsto\mathsf{h}(\mathsf{1}),z\mapsto\mathsf{2}\}\\ &\mbox{where}~{}\mathsf{h}(y)\sigma=\mathsf{h}(\mathsf{1})\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>\mathsf{h}(\mathsf{1})=w\sigma\\ &\mbox{and}~{}\mathsf{first}(x,w)\sigma=\mathsf{first}(\mathsf{2},\mathsf{h}(\mathsf{1}))\stackrel{{\scriptstyle\mathsf{\epsilon}}}{{\rightarrow}}_{\mathcal{R}}\mathsf{2}=z\sigma\end{array}$$

Following the scheme above, we would produce the following pcDCTRS

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{f}^{\mathtt{i}}(x,y)~{}&\to\hfil~{}&\langle z,\beta_{1}(w_{1},w_{2})\rangle\Leftarrow\mathsf{h}^{\mathtt{i}}(y)\twoheadrightarrow\langle w,w_{1}\rangle,~{}\mathsf{first}^{\mathtt{i}}(x,w)\twoheadrightarrow\langle z,w_{2}\rangle\\ \mathsf{h}^{\mathtt{i}}(\mathsf{0})~{}&\to\hfil~{}&\langle\mathsf{0},\beta_{2}\rangle\\ \mathsf{first}^{\mathtt{i}}(x,y)~{}&\to\hfil~{}&\langle x,\beta_{3}(y)\rangle\\ \end{array}$$

Unfortunately, the corresponding reduction for $\mathsf{f}^{\mathtt{i}}(\mathsf{2},\mathsf{1})$ above cannot be done in this system since $\textsf{h}^{\mathtt{i}}(\textsf{1})$ cannot be reduced to $\langle\textsf{h}^{\mathtt{i}}(\textsf{1}),[\,]\rangle$.

In order to overcome this drawback, one could complete the function definitions with rules that reduce each irreducible term $t$ to a tuple of the form $\langle t,[\,]\rangle$. Although we find it a promising idea for future work, in this paper we propose a simpler approach. In the following, we consider a refinement of innermost reduction where only constructor substitutions are computed. Formally, the constructor reduction relation, $\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}$, is defined as follows: given ground terms $s,t\in{\mathcal{T}}({\mathcal{F}})$, we have $s\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{\mathcal{R}}t$ iff there exist a position $p$ in $s$ such that no proper subterms of $s|_{p}$ are reducible, a rewrite rule $l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a ground constructor substitution $\sigma$ such that $s|_{p}=l\sigma$, $s_{i}\sigma\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}\!\!{}^{\ast}_{\mathcal{R}}\>t_{i}\sigma$ for all $i=1,\ldots,n$, and $t=s[r\sigma]_{p}$. Note that the results in the previous section also hold for $\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}$.

In the following, given a basic term $t=\mathsf{f}(\overline{s})$, we denote by $t^{\mathtt{i}}$ the term $\mathsf{f}^{\mathtt{i}}(\overline{s})$. Now, we introduce our injectivization transformation as follows:

Definition 31 (injectivization)

Let ${\mathcal{R}}$ be a pcDCTRS. We produce a new CTRS $\mathbf{I}({\mathcal{R}})$ by replacing each rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}$ of ${\mathcal{R}}$ by a new rule of the form

$$l^{\mathtt{i}}\to\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\Leftarrow\overline{s_{n}^{\mathtt{i}}\twoheadrightarrow\langle t_{n},w_{n}\rangle}$$

in $\mathbf{I}({\mathcal{R}})$, where $\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$ and $\overline{w_{n}}$ are fresh variables. Here, we assume that the variables of $\overline{y}$ are in lexicographic order.

Observe that now we do not need to keep a trace in each term, but only a single trace term since all reductions finish in one step in a pcDCTRS. The relation between the original trace terms and the information stored in the injectivized system is formalized as follows:

Definition 32

Given a trace term $\pi=\beta(\{\overline{y_{m}\mapsto t_{m}}\},\pi_{1},\ldots,\pi_{n})$, we define $\widehat{\pi}$ recursively as follows: $\widehat{\pi}=\beta(\overline{t_{m}},\widehat{\pi_{1}},\ldots,\widehat{\pi_{n}})$, where we assume that the variables $\overline{y_{m}}$ are in lexicographic order.

Moreover, in order to simplify the notation, we consider that a a trace term $\pi$ and a singleton list of the form $[\pi]$ denote the same object. The correctness of the injectivization transformation is stated as follows:

Theorem 33

Let ${\mathcal{R}}$ be a pcDCTRS and ${\mathcal{R}}_{f}=\mathbf{I}({\mathcal{R}})$ be its injectivization. Then ${\mathcal{R}}_{f}$ is a pcDCTRS and, given a basic ground term $s$, we have $\langle s,[\,]\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\rightharpoonup}}_{\mathcal{R}}\langle t,\pi\rangle$ iff $s^{\mathtt{i}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\langle t,\widehat{\pi}\rangle$.

Proof 12

The fact that ${\mathcal{R}}_{f}$ is a pcDCTRS is trivial. Regarding the second part, we proceed as follows:

$(\Rightarrow)$ We proceed by induction on the depth $k$ of the step $\langle s,[\,]\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\rightharpoonup}}_{{\mathcal{R}}_{k}}\langle t,\pi\rangle$. Since the depth $k=0$ is trivial, we consider the inductive case $k>0$. Thus, there is a rule $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$, and a substitution $\sigma$ such that $s=l\sigma$, $\langle s_{i}\sigma,[\,]\rangle{\stackrel{{\scriptstyle\mathsf{c}}}{{\rightharpoonup}}\!\!{}_{{\mathcal{R}}_{k_{i}}}}\langle t_{i}\sigma,\pi_{i}\rangle$, $i=1,\ldots,n$, $t=r\sigma$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$, and $\pi=\beta(\sigma^{\prime},\pi_{1},\ldots,\pi_{n})$. By definition of $\rightharpoonup_{{\mathcal{R}}_{k}}$, we have that $k_{i}<k$ for all $i=1,\ldots,n$ and, thus, by the induction hypothesis, we have $(s_{i}\sigma)^{\mathtt{i}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\>\langle t_{i}\sigma,\widehat{\pi}_{i}\rangle$ for all $i=1,\ldots,n$. Consider now the equivalent rule in ${\mathcal{R}}_{f}$: $l^{\mathtt{i}}\to\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\Leftarrow s_{1}^{\mathtt{i}}\twoheadrightarrow\langle t_{1},w_{1}\rangle,\ldots,s_{n}^{\mathtt{i}}\twoheadrightarrow\langle t_{n},w_{n}\rangle$. Therefore, we have $s^{\mathtt{i}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{f}}\langle t,\beta(\overline{y}\sigma,\widehat{\pi}_{1},\ldots,\widehat{\pi}_{n})\rangle$ where $\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$ and, thus, we can conclude that $\widehat{\pi}=\beta(\overline{y}\sigma,\widehat{\pi}_{1},\ldots,\widehat{\pi}_{n})$.

$(\Leftarrow)$ This direction is analogous. We proceed by induction on the depth $k$ of the step $s^{\mathtt{i}}\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{f_{k}}}\>\langle t,\widehat{\pi}\rangle$. Since the depth $k=0$ is trivial, we consider the inductive case $k>0$. Thus, there is a rule $l^{\mathtt{i}}\to\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\Leftarrow s_{1}^{\mathtt{i}}\twoheadrightarrow\langle t_{1},w_{1}\rangle,\ldots,s_{n}^{\mathtt{i}}\twoheadrightarrow\langle t_{n},w_{n}\rangle$ in ${\mathcal{R}}_{f}$ and a substitution $\theta$ such that $l^{\mathtt{i}}\theta=s^{\mathtt{i}}$, $s^{\mathtt{i}}_{i}\theta\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{f_{k_{i}}}}\langle t_{i},w_{i}\rangle\theta$, $i=1,\ldots,n$, and $\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\theta=\langle t,\widehat{\pi}\rangle$. Assume that $\sigma$ is the restriction of $\theta$ to the variables of the rule, excluding the fresh variables $\overline{w_{n}}$, and that $w_{i}\theta=\widehat{\pi}_{i}$ for all $i=1,\ldots,n$. Therefore, $\langle s_{i},[\,]\rangle\theta=\langle s_{i}\sigma,[\,]\rangle$ and $\langle t_{i},w_{i}\rangle\theta=\langle t_{i}\sigma,\widehat{\pi}_{i}\rangle$, $i=1,\ldots,n$. Then, by definition of ${\mathcal{R}}_{f_{k_{i}}}$, we have that $k_{i}<k$ for all $i=1,\ldots,n$ and, thus, by the induction hypothesis, we have $\langle s_{i}\sigma,[\,]\rangle{\stackrel{{\scriptstyle\mathsf{c}}}{{\rightharpoonup}}\!\!{}_{{\mathcal{R}}}}\langle t_{i}\sigma,\pi_{i}\rangle$, $i=1,\ldots,n$. Consider now the equivalent rule in ${\mathcal{R}}$: $\beta:l\to r\Leftarrow\overline{s_{n}\twoheadrightarrow t_{n}}\in{\mathcal{R}}$. Therefore, we have $\langle s,[\,]\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\rightharpoonup}}_{\mathcal{R}}\langle t,\pi\rangle$, $\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})}$, and $\pi=\beta(\sigma^{\prime},\pi_{1},\ldots,\pi_{n})$. Finally, since $\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(l)\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1,n}})$, we can conclude that $\widehat{\pi}=\pi$.

5.2 Inversion

Given an injectivized system, inversion basically amounts to switching the left- and right-hand sides of the rule and of every equation in the condition, as follows:

Definition 34 (inversion)

Let ${\mathcal{R}}$ be a pcDCTRS and ${\mathcal{R}}_{f}=\mathbf{I}({\mathcal{R}})$ be its injectivization. The inverse system ${\mathcal{R}}_{b}=\mathbf{I}^{-1}({\mathcal{R}}_{f})$ is obtained from ${\mathcal{R}}_{f}$ by replacing each rule

$$\mathsf{f}^{\mathtt{i}}(\overline{s_{0}})\to\langle r,\beta(\overline{y},\overline{w_{n}})\rangle\Leftarrow\mathsf{f}_{1}^{\mathtt{i}}(\overline{s_{1}})\twoheadrightarrow\langle t_{1},w_{1}\rangle,\ldots,\mathsf{f}_{n}^{\mathtt{i}}(\overline{s_{n}})\twoheadrightarrow\langle t_{n},w_{n}\rangle$$

of ${\mathcal{R}}_{f}$ by a new rule of the form

$$\mathsf{f}^{-1}(r,\beta(\overline{y},\overline{w_{n}}))\to\langle\overline{s_{0}}\rangle\Leftarrow\mathsf{f}_{n}^{-1}(t_{n},w_{n})\twoheadrightarrow\langle\overline{s_{n}}\rangle,\ldots,\mathsf{f}_{1}^{-1}(t_{1},w_{1})\twoheadrightarrow\langle\overline{s_{1}}\rangle$$

in $\mathbf{I}^{-1}({\mathcal{R}}_{f})$, where the variables of $\overline{y}$ are in lexicographic order.

Example 35

Consider again the pcDCTRS of Example 16. Here, injectivization returns the following pcDCTRS $\mathbf{I}({\mathcal{R}})={\mathcal{R}}_{f}$:

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{f}^{\mathtt{i}}(x,y,m)~{}&\to\hfil~{}&\langle\mathsf{s}(w),\beta_{1}(m,x,w_{1},w_{2})\rangle\\ ~{}&\hfil~{}&\mbox{}\hskip 8.61108pt\Leftarrow\mathsf{h}^{\mathtt{i}}(x)\twoheadrightarrow\langle x,w_{1}\rangle,\mathsf{g}^{\mathtt{i}}(y,\mathsf{4})\twoheadrightarrow\langle w,w_{2}\rangle\\ \mathsf{h}^{\mathtt{i}}(\mathsf{0})~{}&\to\hfil~{}&\langle\mathsf{0},\beta_{2}\rangle\\ \mathsf{h}^{\mathtt{i}}(\mathsf{1})~{}&\to\hfil~{}&\langle\mathsf{1},\beta_{3}\rangle\\ \mathsf{g}^{\mathtt{i}}(x,y)~{}&\to\hfil~{}&\langle x,\beta_{4}(y)\rangle\\ \end{array}$$

Then, inversion with $\mathbf{I}^{-1}$ produces the following pcDCTRS $\mathbf{I}^{-1}(\mathbf{I}({\mathcal{R}}))={\mathcal{R}}_{b}$:

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{f}^{-1}(\mathsf{s}(w),\beta_{1}(m,x,w_{1},w_{2}))~{}&\to\hfil~{}&\langle x,y,m\rangle\\ ~{}&\hfil~{}&\mbox{}\hskip 8.61108pt\Leftarrow\mathsf{g}^{-1}(w,w_{2})\twoheadrightarrow\langle y,\mathsf{4}\rangle,\mathsf{h}^{-1}(x,w_{1})\twoheadrightarrow\langle x\rangle\\ \mathsf{h}^{-1}(\mathsf{0},\beta_{2})~{}&\to\hfil~{}&\langle\mathsf{0}\rangle\\ \mathsf{h}^{-1}(\mathsf{1},\beta_{3})~{}&\to\hfil~{}&\langle\mathsf{1}\rangle\\ \mathsf{g}^{-1}(x,\beta_{4}(y))~{}&\to\hfil~{}&\langle x,y\rangle\\ \end{array}$$

Finally, the correctness of the inversion transformation is stated as follows:

Theorem 36

Let ${\mathcal{R}}$ be a pcDCTRS, ${\mathcal{R}}_{f}=\mathbf{I}({\mathcal{R}})$ its injectivization, and ${\mathcal{R}}_{b}=\mathbf{I}^{-1}({\mathcal{R}}_{f})$ the inversion of ${\mathcal{R}}_{f}$. Then, ${\mathcal{R}}_{b}$ is a basic pcDCTRS and, given a basic ground term $\mathsf{f}(\overline{s})$ and a constructor ground term $t$ with $\langle t,\pi\rangle$ a safe pair, we have $\langle t,\pi\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\leftharpoondown}}_{\mathcal{R}}\langle\mathsf{f}(\overline{s}),[\,]\rangle$ iff $\mathsf{f}^{-1}(t,\widehat{\pi})\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{b}}\>\langle\overline{s}\rangle$.

Proof 13

The fact that ${\mathcal{R}}_{f}$ is a pcDCTRS is trivial. Regarding the second part, we proceed as follows.

$(\Rightarrow)$ We proceed by induction on the depth $k$ of the step $\langle t,\pi\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\leftharpoondown}}_{{\mathcal{R}}_{k}}\langle\mathsf{f}(\overline{s}),[\,]\rangle$. Since the depth $k=0$ is trivial, we consider the inductive case $k>0$. Let $\pi=\beta(\sigma^{\prime},\overline{\pi_{n}})$. Thus, we have that $\langle t,\beta(\sigma^{\prime},\overline{\pi_{n}})\rangle$ is a safe pair, there is a rule $\beta:\mathsf{f}(\overline{s_{0}})\to r\Leftarrow\mathsf{f}_{1}(\overline{s_{1}})\twoheadrightarrow t_{1},\ldots,\mathsf{f}_{n}(\overline{s_{n}})\twoheadrightarrow t_{n}$ and substitution $\theta$ with $\mathsf{{{\mathcal{D}}}om}(\theta)=(\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{1}},\ldots,\overline{s_{n}})\backslash\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime}))$ such that $t=r\theta$, $\langle t_{i}\theta\sigma^{\prime},\pi_{i}\rangle{\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{k_{i}}}}\langle\mathsf{f}(\overline{s_{i}})\theta\sigma^{\prime},[\,]\rangle$ for all $i=1,\ldots,n$, and $\mathsf{f}(\overline{s})=\mathsf{f}(\overline{s_{0}})\theta\sigma^{\prime}$. Note that $\overline{s_{0}},\ldots,\overline{s_{n}}$ denote sequences of terms of arbitrary length, i.e., $\overline{s_{0}}=s_{0,1},\ldots,s_{0,l_{0}}$, $\overline{s_{1}}=s_{1,1},\ldots,s_{1,l_{1}}$, etc. Since $\langle t,\pi\rangle$ is a safe pair, we have that $\mathsf{{{\mathcal{D}}}om}(\sigma^{\prime})=(\mathsf{{{\mathcal{V}}}ar}(\overline{s_{0}})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{1}},\ldots,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1}},\ldots,\overline{s_{n}})$. By definition of $\leftharpoondown_{{\mathcal{R}}_{k}}$, we have that $k_{i}<k$ for all $i=1,\ldots,n$ and, by the induction hypothesis, we have $\mathsf{f}^{-1}(t_{i}\sigma,\widehat{\pi_{i}}){\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{b}}}\langle\overline{s_{i}}\sigma\rangle$ for all $i=1,\ldots,n$. Let us now consider the equivalent rule in ${\mathcal{R}}_{b}$:

$$\mathsf{f}^{-1}(r,\beta(\overline{y},\overline{w_{n}})))\to\langle\overline{s_{0}}\rangle\Leftarrow\mathsf{f}_{n}^{-1}(t_{n},w_{n})\twoheadrightarrow\langle\overline{s_{n}}\rangle,\ldots,\mathsf{f}_{1}^{-1}(t_{1},w_{1})\twoheadrightarrow\langle\overline{s_{1}}\rangle$$

Hence, we have $\mathsf{f}^{-1}(t,\beta(\overline{y}\sigma,\widehat{\pi}_{1},\ldots,\widehat{\pi}_{1}))\to_{{\mathcal{R}}_{b}}\langle\overline{s_{0}}\sigma\rangle=\langle\overline{s}\rangle$, where

$$\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(\overline{s_{0}})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{1}},\ldots,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1}},\ldots,\overline{s_{n}})$$

and, thus, we can conclude that $\widehat{\pi}=\beta(\overline{y}\sigma,\widehat{\pi}_{1},\ldots,\widehat{\pi}_{n})$.

$(\Leftarrow)$ This direction is analogous. We proceed by induction on the depth $k$ of the step $\mathsf{f}^{-1}(t,\widehat{\pi})\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{b_{k}}}\langle\overline{s}\rangle$. Since the depth $k=0$ is trivial, we consider the inductive case $k>0$. Thus, there is a rule $\mathsf{f}^{-1}(r,\beta(\overline{y},\overline{w_{n}})))\to\langle\overline{s_{0}}\rangle\Leftarrow\mathsf{f}_{n}^{-1}(t_{n},w_{n})\twoheadrightarrow\langle\overline{s_{n}}\rangle,\ldots,\mathsf{f}_{1}^{-1}(t_{1},w_{1})\twoheadrightarrow\langle\overline{s_{1}}\rangle$ in ${\mathcal{R}}_{b}$ and a substitution $\theta$ such that $\mathsf{f}^{-1}(r,\beta(\overline{y},\overline{w_{n}}))\theta=\mathsf{f}^{-1}(t,\widehat{\pi})$, $\mathsf{f}_{i}^{-1}(t_{i},w_{i})\theta\stackrel{{\scriptstyle\mathsf{c}}}{{\rightarrow}}_{{\mathcal{R}}_{b_{k_{i}}}}\langle\overline{s_{i}}\rangle\theta$, $i=n,\ldots,1$, and $\mathsf{f}^{-1}(r,ws)\theta=\langle\overline{s}\rangle$. Assume that $\sigma$ is the restriction of $\theta$ to the variables of the rule, excluding the fresh variables $\overline{w_{n}}$, and that $w_{i}\theta=\widehat{\pi}_{i}$ for all $i=1,\ldots,n$. Therefore, $\mathsf{f}^{-1}(r,\beta(\overline{y},\overline{w_{n}}))\theta=\mathsf{f}^{-1}(r\sigma,\beta(\overline{y}\sigma,\widehat{\pi}_{1},\ldots,\widehat{\pi}_{n})$, $\mathsf{f}_{i}^{-1}(t_{i},w_{i})\theta=\mathsf{f}_{i}^{-1}(t_{i}\sigma,\widehat{\pi}_{i})$ and $\langle\overline{s_{i}}\rangle\theta=\langle\overline{s_{i}}\sigma\rangle$, $i=1,\ldots,n$. Then, by definition of ${\mathcal{R}}_{b_{k_{i}}}$, we have that $k_{i}<k$ for all $i=1,\ldots,n$ and, thus, by the induction hypothesis, we have $\langle t_{i}\sigma,\pi_{i}\rangle{\stackrel{{\scriptstyle\mathsf{c}}}{{\leftharpoondown}}\!\!{}_{{\mathcal{R}}}}\langle\mathsf{f}_{i}(\overline{s_{i}}\sigma),[\,]\rangle$, $i=1,\ldots,n$. Consider now the equivalent rule in ${\mathcal{R}}$: $\beta:\mathsf{f}(\overline{s_{0}})\to r\Leftarrow\mathsf{f}_{1}(\overline{s_{1}})\twoheadrightarrow t_{1},\ldots,\mathsf{f}_{n}(\overline{s_{n}})\twoheadrightarrow t_{n}$ in ${\mathcal{R}}$. Therefore, we have $\langle t,\pi\rangle\stackrel{{\scriptstyle\mathsf{c}}}{{\leftharpoondown}}_{\mathcal{R}}\langle\mathsf{f}(\overline{s}),[\,]\rangle$,

$$\sigma^{\prime}=\sigma\!\!\mathrel{|\grave{}}_{(\mathsf{{{\mathcal{V}}}ar}(\overline{s_{0}})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{1}},\ldots,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1}},\ldots,\overline{s_{n}})}$$

and $\pi=\beta(\sigma^{\prime},\pi_{1},\ldots,\pi_{n})$. Finally, since $\{\overline{y}\}=(\mathsf{{{\mathcal{V}}}ar}(\overline{s_{0}})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{1}},\ldots,\overline{s_{n}},\overline{t_{n}}))\cup\bigcup_{i=1}^{n}\mathsf{{{\mathcal{V}}}ar}(t_{i})\backslash\mathsf{{{\mathcal{V}}}ar}(r,\overline{s_{i+1}},\ldots,\overline{s_{n}})$, we can conclude that $\widehat{\pi}=\pi$.

5.3 Improving the transformation for injective functions

When a function is injective, one can expect the injectivization transformation to be unnecessary. This is not generally true, since some additional syntactic conditions might also be required. Furthermore, depending on the considered setting, it can be necessary to have an injective system, rather than an injective function. Consider, e.g., the following simple TRS:

$${\mathcal{R}}=\{~{}\mathsf{f_{1}}\to\mathsf{f_{2}},\mathsf{f_{2}}\to\mathsf{0},~{}\mathsf{g_{1}}\to\mathsf{g_{2}},~{}\mathsf{g_{2}}\to\mathsf{0}~{}\}$$

Here, all functions are clearly injective. However, given a reduction like $\mathsf{f_{1}}\to_{\mathcal{R}}\mathsf{f_{2}}\to_{\mathcal{R}}\mathsf{0}$, we do not know which rule should be applied to $\mathsf{0}$ in order to go backwards until the initial term (actually, both the second and the fourth rules are applicable in the reverse direction).

Luckily, in our context, the injectivity of a function suffices since reductions in pcDCTRSs are performed in a single step. Therefore, given a reduction of the form $\mathsf{f}^{\mathtt{i}}(\overline{s_{n}})\to_{\mathcal{R}}t$, a backward computation will have the form $\mathsf{f}^{-1}(t)\to_{\mathcal{R}}\langle\overline{s_{n}}\rangle$, so that we know that only the inverse rules of $\mathsf{f}$ are applicable.

Now, we present an improvement of the injectivization transformation presented in Section 5.1 which has some similarities with that in [24]. Here, we consider that the initial system is a TRS ${\mathcal{R}}$ since, to the best of our knowledge, there is no reachability analysis defined for DCTRSs. In the following, given a term $s$, we let

$$\mathsf{range}(s)=\{t\mid s\sigma\to_{\mathcal{R}}^{\ast}t,~{}\sigma:{\mathcal{V}}\mapsto{\mathcal{T}}({\mathcal{C}}),~{}\mbox{and}~{}t\in{\mathcal{T}}({\mathcal{C}})\}$$

i.e., $\mathsf{range}(s)$ returns a set with the constructor normal forms of all possible ground constructor instances of $s$. Although computing this set is generally undecidable, there are some overapproximations based on the use of tree automata (see, e.g., [15] and the most recent approach for innermost rewriting [16]). Let us consider that $\mathsf{range}^{\alpha}(s)$ is such an approximation, with $\mathsf{range}^{\alpha}(s)\supseteq\mathsf{range}(s)$ for all terms $s$. Here, we are interested in determining when the right-hand sides, $r_{1}$ and $r_{2}$, of two rules do not overlap, i.e., $\mathsf{range}(r_{1})\cap\mathsf{range}(r_{2})=\varnothing$. For this purpose, we will check whether $\mathsf{range}^{\alpha}(r_{1})\cap\mathsf{range}^{\alpha}(r_{2})=\varnothing$. Since finite tree automata are closed under intersection and the emptiness of a finite tree automata is decidable, checking the emptiness of $\mathsf{range}^{\alpha}(r_{1})\cap\mathsf{range}^{\alpha}(r_{2})$ is decidable and can be used to safely identify non-overlapping right-hand sides, i.e., if $\mathsf{range}^{\alpha}(r_{1})\cap\mathsf{range}^{\alpha}(r_{2})=\varnothing$, then $r_{1}$ and $r_{2}$ are definitely non-overlapping; otherwise, they may be overlapping or non-overlapping.

Now, we summarize our method to simplify some trace terms. Given a constructor TRS ${\mathcal{R}}$ and a rule $\beta:l\to r\in{\mathcal{R}}$, we check the following conditions:

1. the right-hand side $r$ of the rule does not overlap with the right-hand side of any other rule defining the same function;

2. the rule is non-erasing, i.e., $\mathsf{{{\mathcal{V}}}ar}(l)=\mathsf{{{\mathcal{V}}}ar}(r)$;

3. the right-hand side $r$ contains a single occurrence of a defined function symbol, say $\mathsf{f}\in{\mathcal{D}}$.

If these conditions hold, then the rule has the form $l\to r[\mathsf{f}(\overline{s})]_{p}$ with $l$ and $\mathsf{f}(\overline{s})$ basic terms, and $r[x]_{p}$ and $\overline{s}$ constructor terms, where $x$ is a fresh variable. In this case, we can safely produce the following injective version:

$$l^{\mathtt{i}}\to\langle r[x]_{p},w\rangle\Leftarrow\mathsf{f}^{\mathtt{i}}(\overline{s})\twoheadrightarrow\langle x,w\rangle$$

instead of

$$l^{\mathtt{i}}\to\langle r[x]_{p},\beta(w)\rangle\Leftarrow\mathsf{f}^{\mathtt{i}}(\overline{s})\twoheadrightarrow\langle x,w\rangle$$

Let us illustrate this improved transformation with a couple of examples.

Example 37

Consider the following TRS:

$${\mathcal{R}}=\{~{}\mathsf{f}(\mathsf{s}(x))\to\mathsf{g}(x),~{}\mathsf{f}(\mathsf{c}(x))\to\mathsf{h}(x),~{}\mathsf{g}(x)\to\mathsf{s}(x),~{}\mathsf{h}(x)\to\mathsf{c}(x)\}$$

Here, it can easily be shown that $\mathsf{range}^{\alpha}(\mathsf{g}(x))\cap\mathsf{range}^{\alpha}(\mathsf{h}(x))=\varnothing$, the two rules defining $\mathsf{f}$ are non-erasing, and both contain a single occurrence of a defined function symbol in the righ-hand sides. Therefore, our improved injectivization applies and we get the following pcDCTRS ${\mathcal{R}}_{f}$:

$$\begin{array}[]{r@{~}c@{~}l@{~~~~~~~~~}r@{~}c@{~}l}\mathsf{f}^{\mathtt{i}}(\mathsf{s}(x))~{}&\to\hfil~{}&\langle y,w\rangle\Leftarrow\mathsf{g}^{\mathtt{i}}(x)\twoheadrightarrow\langle y,w\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{g}^{\mathtt{i}}(x)~{}&\to\hfil~{}&\langle\mathsf{s}(x),\beta_{3}\rangle\\ \mathsf{f}^{\mathtt{i}}(\mathsf{c}(x))~{}&\to\hfil~{}&\langle y,w\rangle\Leftarrow\mathsf{h}^{\mathtt{i}}(x)\twoheadrightarrow\langle y,w\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{h}^{\mathtt{i}}(x)~{}&\to\hfil~{}&\langle\mathsf{c}(x),\beta_{4}\rangle\end{array}$$

In contrast, the original injectivization transformation would return the following system:

$$\begin{array}[]{r@{~}c@{~}l@{~~~~~~~~~}r@{~}c@{~}l}\mathsf{f}^{\mathtt{i}}(\mathsf{s}(x))~{}&\to\hfil~{}&\langle y,\beta_{1}(w)\rangle\Leftarrow\mathsf{g}^{\mathtt{i}}(x)\twoheadrightarrow\langle y,w\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{g}^{\mathtt{i}}(x)~{}&\to\hfil~{}&\langle\mathsf{s}(x),\beta_{3}\rangle\\ \mathsf{f}^{\mathtt{i}}(\mathsf{c}(x))~{}&\to\hfil~{}&\langle y,\beta_{2}(w)\rangle\Leftarrow\mathsf{h}^{\mathtt{i}}(x)\twoheadrightarrow\langle y,w\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{h}^{\mathtt{i}}(x)~{}&\to\hfil~{}&\langle\mathsf{c}(x),\beta_{4}\rangle\end{array}$$

Finally, the inverse system ${\mathcal{R}}_{b}$ obtained from ${\mathcal{R}}_{f}$ using the original transformation has the following form:

$$\begin{array}[]{r@{~}c@{~}l@{~~~~~~~~~}r@{~}c@{~}l}\mathsf{f}^{-1}(y,w)~{}&\to\hfil~{}&\langle\mathsf{s}(x)\rangle\Leftarrow\mathsf{g}^{-1}(y,w)\twoheadrightarrow\langle x\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{g}^{-1}(\mathsf{s}(x),\beta_{3})~{}&\to\hfil~{}&\langle x\rangle\\ \mathsf{f}^{-1}(y,w)~{}&\to\hfil~{}&\langle\mathsf{c}(x)\rangle\Leftarrow\mathsf{h}^{-1}(y,w)\twoheadrightarrow\langle x\rangle\hfil~{}~{}~{}~{}~{}~{}~{}~{}~{}&\mathsf{h}^{-1}(\mathsf{c}(x),\beta_{4})~{}&\to\hfil~{}&\langle x\rangle\end{array}$$

For instance, given the forward reduction $\mathsf{f}^{\mathtt{i}}(\mathsf{s}(\mathsf{0}))\to_{{\mathcal{R}}_{f}}\langle\mathsf{s}(\mathsf{0}),\beta_{3}\rangle$, we can build the corresponding backward reduction: $\mathsf{f}^{-1}(\mathsf{s}(\mathsf{0}),\beta_{3})\to_{{\mathcal{R}}_{b}}\langle\mathsf{s}(\mathsf{0})\rangle$.

Note, however, that the left-hand sides of $\mathsf{f}^{-1}$ overlap and we should reduce the conditions in order to determine which rule to apply. Therefore, in some cases, there is a trade-off between the size of the trace terms and the complexity of the reduction steps.

The example above, though, only produces a rather limited improvement since the considered functions are not recursive. Our next example shows a much significant improvement. Here, we consider the function $\mathsf{zip}$ (also used in [24] to illustrate the benefits of an injectivity analysis).

Example 38

Consider the following TRS ${\mathcal{R}}$ defining the function $\mathsf{zip}$:

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{zip}([\,],ys)~{}&\to\hfil~{}&[\,]\\ \mathsf{zip}(xs,[\,])~{}&\to\hfil~{}&[\,]\\ \mathsf{zip}(x:xs,y:ys)~{}&\to\hfil~{}&\mathsf{pair}(x,y):\mathsf{zip}(xs,ys)\\ \end{array}$$

Here, since the third rule is non-erasing, its right-hand side contains a single occurrence of a defined function, $\mathsf{zip}$, and it does not overlap with any other right-hand side, our improved injectivization applies and we get the following pcDCTRS ${\mathcal{R}}_{f}$:

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{zip}^{\mathtt{i}}([\,],ys)~{}&\to\hfil~{}&\langle[\,],\beta_{1}(ys)\rangle\\ \mathsf{zip}^{\mathtt{i}}(xs,[\,])~{}&\to\hfil~{}&\langle[\,],\beta_{2}(xs)\rangle\\ \mathsf{zip}^{\mathtt{i}}(x:xs,y:ys)~{}&\to\hfil~{}&\langle\mathsf{pair}(x,y):zs,w\rangle\Leftarrow\mathsf{zip}^{\mathtt{i}}(xs,ys)\twoheadrightarrow\langle zs,w\rangle\\ \end{array}$$

In contrast, the original injectivization transformation would return the following system ${\mathcal{R}}^{\prime}_{f}$:

$$\begin{array}[]{r@{~}c@{~}l}\mathsf{zip}^{\mathtt{i}}([\,],ys)~{}&\to\hfil~{}&\langle[\,],\beta_{1}(ys)\rangle\\ \mathsf{zip}^{\mathtt{i}}(xs,[\,])~{}&\to\hfil~{}&\langle[\,],\beta_{2}(xs)\rangle\\ \mathsf{zip}^{\mathtt{i}}(x:xs,y:ys)~{}&\to\hfil~{}&\langle\mathsf{pair}(x,y):zs,\beta_{3}(w)\rangle\Leftarrow\mathsf{zip}^{\mathtt{i}}(xs,ys)\twoheadrightarrow\langle zs,w\rangle\\ \end{array}$$

It might seem a small difference, but if we call $\mathsf{zip}^{\mathtt{i}}$ with two lists of $n$ elements, the system ${\mathcal{R}}^{\prime}_{f}$ would build a trace term of the form $\beta_{3}(\ldots\beta_{3}(\beta_{1}(\ldots))\ldots)$ with $n$ nested constructors $\beta_{3}$, while ${\mathcal{R}}_{f}$ would just build the trace term $\beta_{1}(\ldots)$. For large values of $n$, this is a significant improvement in memory usage.

6 Bidirectional Program Transformation

We illustrate a practical application of our reversibilization technique in the context of bidirectional program transformation (see [10] for a survey). In particular, we consider the so-called view-update problem. Here, we have a data structure (e.g., a database) called the source, which is transformed to another data structure, called the view. Typically, we have a view function, $\mathsf{view}\!\!:\mathit{Source}\to\mathit{View}$ that takes the source and returns the corresponding view, together with an update function, $\mathsf{upd}\!\!:\mathit{View}\times\mathit{Source}\to\mathit{Source}$ that propagates the changes in a modified view to the original source. Two basic properties that these functions should satisfy in order to be well-behaved are the following [13]:

$$\begin{array}[]{r@{}cl}\forall s\in\mathit{Source},\forall v\in\mathit{View}&:&\mathsf{view}(\mathsf{upd}(v,s))=v\\ \forall s\in\mathit{Source}&:&\mathsf{upd}(\mathsf{view}(s),s)=s\end{array}$$

Bidirectionalization (first proposed in the database community [5]) basically consists in, given a view function, “bidirectionalize” it in order to derive an appropriate update function. For this purpose, first, a view complement function is usually defined, say $\mathsf{view}^{c}$, so that the tupled function

$$\mathsf{view}\vartriangle\mathsf{view}^{c}\!\!:\mathit{Source}\to\mathit{View}\times\mathit{Comp}$$

becomes injective. Therefore, the update function can be defined as follows:

$$\mathsf{upd}(v,s)=(\mathsf{view}\vartriangle\mathsf{view}^{c})^{-1}(v,\mathsf{view}^{c}(s))$$

This approach has been applied to bidirectionalize view functions in a functional language in [24].

In the following, we apply our injectivization and inversion transformations in order to produce a bidirectionalization transformation that may be useful in the context of the view-update problem (with some limitations). Let us assume that we have a view function, $\mathsf{view}$, that takes a source and returns the corresponding view, and which is defined by means of a pcDCTRS. Following our approach, given the original program ${\mathcal{R}}$, we produce an injectivized version ${\mathcal{R}}_{f}$ and the corresponding inverse ${\mathcal{R}}_{b}$. Therefore, in principle, one can use ${\mathcal{R}}_{f}\cup{\mathcal{R}}_{b}$, which will include the functions $\mathsf{view}^{\mathtt{i}}$ and $\mathsf{view}^{-1}\!$, to define an update function as follows:

$$\mathsf{upd}(v,s)\to s^{\prime}\Leftarrow\mathsf{view}^{\mathtt{i}}(s)\twoheadrightarrow\langle v^{\prime},\pi\rangle,\mathsf{view}^{-1}\!(v,\pi)\twoheadrightarrow\langle s^{\prime}\rangle$$

where $s$ is the original source, $v$ is the updated view, and $s^{\prime}$, the returned value, is the corresponding updated source. Note that, in our context, the function $\mathsf{view}^{\mathtt{i}}$ is somehow equivalent to $\mathsf{view}\vartriangle\mathsf{view}^{c}$ above.

Let us now illustrate the bidirectionalization process with an example. Consider a particular data structure, a list of records of the form $\mathsf{r}(t,v)$ where $t$ is the type of the record (e.g., $\mathsf{book}$, $\mathsf{dvd}$, $\mathsf{pen}$, etc.) and $v$ is its price tag. The following system defines a view function that takes a type and a list of records, and returns a list with the price tags of the records of the given type:

$$\begin{array}[]{rcl}\mathsf{view}(t,\mathsf{nil})&\to&\mathsf{nil}\\ \mathsf{view}(t,\mathsf{r}(t^{\prime},v):rs)&\to&\mathsf{val}(\mathsf{r}(t^{\prime},v)):\mathsf{view}(t,rs)\Leftarrow\mathsf{eq}(t,t^{\prime})\twoheadrightarrow\mathsf{true}\\ \mathsf{view}(t,\mathsf{r}(t^{\prime},v):rs)&\to&\mathsf{view}(t,rs)\Leftarrow\mathsf{eq}(t,t^{\prime})\twoheadrightarrow\mathsf{false}\\ \mathsf{eq}(\mathsf{book},\mathsf{book})&\to&\mathsf{true}\hskip 43.05542pt\mathsf{eq}(\mathsf{dvd},\mathsf{dvd})~{}\to~{}\mathsf{true}\\ \mathsf{eq}(\mathsf{book},\mathsf{dvd})&\to&\mathsf{false}\hskip 41.33322pt\mathsf{eq}(\mathsf{dvd},\mathsf{book})~{}\to~{}\mathsf{false}\\ \mathsf{val}(\mathsf{r}(t,v))&\to&v\\ \end{array}$$

However, this system is not a pcDCTRS. Here, we use a flattening transformation to produce the following (labeled) pcDCTRS ${\mathcal{R}}$ which is equivalent for constructor derivations:

$$\begin{array}[]{lr@{~}c@{~}l}\beta_{1}:&\mathsf{view}(t,\mathsf{nil})~{}&\to\hfil~{}&\mathsf{nil}\\ \beta_{2}:&\mathsf{view}(t,\mathsf{r}(t^{\prime},v):rs)~{}&\to\hfil~{}&p:r\\ &~{}&\hfil~{}&\mbox{}\Leftarrow\mathsf{eq}(t,t^{\prime})\twoheadrightarrow\mathsf{true},\mathsf{val}(\mathsf{r}(t^{\prime},v))\twoheadrightarrow p,\mathsf{view}(t,rs)\twoheadrightarrow r\\ \beta_{3}:&\mathsf{view}(t,\mathsf{r}(t^{\prime},v):rs)~{}&\to\hfil~{}&r\Leftarrow\mathsf{eq}(t,t^{\prime})\twoheadrightarrow\mathsf{false},\mathsf{view}(t,rs)\twoheadrightarrow r\\[4.30554pt] \beta_{4}:&\mathsf{eq}(\mathsf{book},\mathsf{book})~{}&\to\hfil~{}&\mathsf{true}\hskip 43.05542pt\beta_{5}:~{}\mathsf{eq}(\mathsf{dvd},\mathsf{dvd})~{}\to~{}\mathsf{true}\\ \beta_{6}:&\mathsf{eq}(\mathsf{book},\mathsf{dvd})~{}&\to\hfil~{}&\mathsf{false}\hskip 40.90265pt\beta_{7}:~{}\mathsf{eq}(\mathsf{dvd},\mathsf{book})~{}\to~{}\mathsf{false}\\[4.30554pt] \beta_{8}:&\mathsf{val}(\mathsf{r}(t,v))~{}&\to\hfil~{}&v\\ \end{array}$$

Now, we can apply our injectivization transformation which returns the following pcDCTRS ${\mathcal{R}}_{f}=\mathbf{I}({\mathcal{R}})$:

$$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{view}^{\mathtt{i}}(t,\mathsf{nil})~{}&\to\hfil~{}&\langle\mathsf{nil},\beta_{1}(t)\rangle\\ \mathsf{view}^{\mathtt{i}}(t,\mathsf{r}(t^{\prime},v):rs)~{}&\to\hfil~{}&\langle p:r,\beta_{2}(w_{1},w_{2},w_{3})\rangle\\ ~{}&\hfil~{}&\mbox{}\Leftarrow\mathsf{eq}^{\mathtt{i}}(t,t^{\prime})\twoheadrightarrow\langle\mathsf{true},w_{1}\rangle,\mathsf{val}^{\mathtt{i}}(\mathsf{r}(t^{\prime},v))\twoheadrightarrow\langle p,w_{2}\rangle,\mathsf{view}^{\mathtt{i}}(t,rs)\twoheadrightarrow\langle r,w_{3}\rangle\\ \mathsf{view}^{\mathtt{i}}(t,\mathsf{r}(t^{\prime},v):rs)~{}&\to\hfil~{}&\langle r,\beta_{3}(v,w_{1},w_{2})\rangle\\ ~{}&\hfil~{}&\mbox{}\Leftarrow\mathsf{eq}^{\mathtt{i}}(t,t^{\prime})\twoheadrightarrow\langle\mathsf{false},w_{1}\rangle,\mathsf{view}^{\mathtt{i}}(t,rs)\twoheadrightarrow\langle r,w_{2}\rangle\\[4.30554pt] \mathsf{eq}^{\mathtt{i}}(\mathsf{book},\mathsf{book})~{}&\to\hfil~{}&\langle\mathsf{true},\beta_{4}\rangle\hskip 47.36096pt\mathsf{eq}^{\mathtt{i}}(\mathsf{dvd},\mathsf{dvd})\>\to\>\langle\mathsf{true},\beta_{5}\rangle\\ \mathsf{eq}^{\mathtt{i}}(\mathsf{book},\mathsf{dvd})~{}&\to\hfil~{}&\langle\mathsf{false},\beta_{6}\rangle\hskip 40.90265pt\mathsf{eq}^{\mathtt{i}}(\mathsf{dvd},\mathsf{book})\>\to\>\langle\mathsf{false},\beta_{7}\rangle\\[4.30554pt] \mathsf{val}^{\mathtt{i}}(\mathsf{r}(t,v))~{}&\to\hfil~{}&\langle v,\beta_{8}(t)\rangle\\ \end{array}$$

Finally, inversion returns the following pcDCTRS ${\mathcal{R}}_{b}=\mathbf{I}({\mathcal{R}}_{f})$:

$$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{view}^{-1}\!(\mathsf{nil},\beta_{1}(t))~{}&\to\hfil~{}&\langle t,\mathsf{nil}\rangle\\ \mathsf{view}^{-1}\!(p:r,\beta_{2}(w_{1},w_{2},w_{3}))~{}&\to\hfil~{}&\langle t,\mathsf{r}(t^{\prime},v):rs\rangle\\ ~{}&\hfil~{}&\mbox{}\Leftarrow\mathsf{eq}^{-1}\!(\mathsf{true},w_{1})\twoheadrightarrow\langle t,t^{\prime}\rangle,\mathsf{val}^{-1}\!(p,w_{2})\twoheadrightarrow\langle\mathsf{r}(t^{\prime},v)\rangle,\mathsf{view}^{-1}\!(r,w_{3})\twoheadrightarrow\langle t,rs\rangle\\ \mathsf{view}^{-1}\!(r,\beta_{3}(v,w_{1},w_{2}))~{}&\to\hfil~{}&\langle t,\mathsf{r}(t^{\prime},v):rs\rangle\\ ~{}&\hfil~{}&\mbox{}\Leftarrow\mathsf{eq}^{-1}\!(\mathsf{false},w_{1})\twoheadrightarrow\langle t,t^{\prime}\rangle,\mathsf{view}^{-1}\!(r,w_{2})\twoheadrightarrow\langle t,rs\rangle\\[4.30554pt] \mathsf{eq}^{-1}\!(\mathsf{true},\beta_{4})~{}&\to\hfil~{}&\langle\mathsf{book},\mathsf{book}\rangle\hskip 10.76385pt\mathsf{eq}^{-1}\!(\mathsf{true},\beta_{5})\>\to\>\langle\mathsf{dvd},\mathsf{dvd}\rangle\\ \mathsf{eq}^{-1}(\mathsf{false},\beta_{6})~{}&\to\hfil~{}&\langle\mathsf{book},\mathsf{dvd}\rangle\hskip 15.0694pt\mathsf{eq}^{-1}\!(\mathsf{false},\beta_{7})\>\to\>\langle\mathsf{dvd},\mathsf{book}\rangle\\[4.30554pt] \mathsf{val}^{-1}\!(v,\beta_{8}(t))~{}&\to\hfil~{}&\langle\mathsf{r}(t,v)\rangle\\ \end{array}$$

For instance, the term $\mathsf{view}(\mathsf{book},[\mathsf{r}(\mathsf{book},\mathsf{12}),\mathsf{r}(\mathsf{dvd},\mathsf{24})])$, reduces to $[\mathsf{12}]$ in the original system ${\mathcal{R}}$. Given a modified view, e.g., $[\mathsf{15}]$, we can compute the modified source using function $\mathsf{upd}$ above:

$$\mathsf{upd}([\mathsf{r}(\mathsf{book},\mathsf{12}),\mathsf{r}(\mathsf{dvd},\mathsf{24})],~{}[\mathsf{15}])$$

Here, we have the following subcomputations:

$$\begin{array}[]{l}\mathsf{view}^{\mathtt{i}}(\mathsf{book},[\mathsf{r}(\mathsf{book},\mathsf{12}),\mathsf{r}(\mathsf{dvd},\mathsf{24})])\\ \hskip 86.11084pt\to_{{\mathcal{R}}_{f}}\langle[\mathsf{12}],\beta_{2}(\beta_{4},\beta_{8}(\mathsf{book}),\beta_{3}(\mathsf{24},\beta_{6},\beta_{1}(\mathsf{book})))\rangle\\ \mathsf{view}^{-1}\!([\mathsf{15}],\beta_{2}(\beta_{4},\beta_{8}(\mathsf{book}),\beta_{3}(\mathsf{24},\beta_{6},\beta_{1}(\mathsf{book}))))\\ \hskip 86.11084pt\to_{{\mathcal{R}}_{b}}\langle\mathsf{book},[\mathsf{r}(\mathsf{book},\mathsf{15}),\mathsf{r}(\mathsf{dvd},\mathsf{24})]\rangle\end{array}$$

Thus $\mathsf{upd}$ returns the updated source $[\mathsf{r}(\mathsf{book},\mathsf{15}),\mathsf{r}(\mathsf{dvd},\mathsf{24})]$, as expected. We note that the considered example cannot be transformed using the technique in [24], the closer to our approach, since the right-hand sides of some rules contain functions which are not treeless. Nevertheless, one could consider a transformation from pcDCTRS to functional programs with treeless functions so that the technique in [24] becomes applicable.

Our approach can solve a view-update problem as long as the view function can be encoded in a pcDCTRS. When this is the case, the results from Section 5 guarantee that function $\mathsf{upd}$ is well defined. Formally analyzing the class of view functions that can be represented with a pcDCTRS is an interesting topic for further research.

7 Related Work

There is no widely accepted notion of reversible computing. In this work, we have considered one of its most popular definitions, according to which a computation principle is reversible if there is a method to undo a (forward) computation. Moreover, we expect to get back to an exact past state of the computation. This is often referred to as full reversibility.

As we have mentioned in the introduction, some of the most promising applications of reversibility include cellular automata [28], bidirectional program transformation [24], already discussed in Section 6, reversible debugging [17], where the ability to go both forward and backward when seeking the cause of an error can be very useful for the programmer, parallel discrete event simulation [34], where reversibility is used to undo the effects of speculative computations made on a wrong assumption, quantum computing [39], where all computations should be reversible, and so forth. The interested reader can find detailed surveys in the state of the art reports of the different working groups of COST Action IC1405 on Reversible Computation [20].

Intuitively speaking, there are two broad approaches to reversibility from a programming language perspective:

Reversible programming languages.

In this case, all constructs of the programming language are reversible. One of the most popular languages within the first approach is the reversible (imperative) language Janus [23]. The language was recently rediscovered [42, 41, 43] and has since been formalized and further developed.

Irreversible programming languages and Landauer’s embedding.

Alternatively, one can consider an irreversible programming language, and enhance the states with some additional information (typically, the history of the computation so far) so that computations become reversible. This is called Landauer’s embedding.

In this work, we consider reversibility in the context of term rewriting. To the best of our knowledge, we have presented the first approach to reversibility in term rewriting. A closest approach was introduced by Abramsky in the context of pattern matching automata [2], though his developments could easily be applied to rewrite systems as well. In Abramsky’s approach, biorthogonality was required to ensure reversibility, which would be a very significant restriction for term rewriting systems. Basically, biorthogonality requires that, for every pair of (different) rewrite rules $l\to r$ and $l^{\prime}\to r^{\prime}$, $l$ and $l^{\prime}$ do not overlap (roughly, they do not unify) and $r$ and $r^{\prime}$ do not overlap too. Trivially, the functions of a biorthogonal system are injective and, thus, computations are reversible without the need of a Landauer embedding. Therefore, Abramsky’s work is aimed at defining a reversible language, in contrast to our approach that is based on defining a Landauer embedding for standard term rewriting and a general class of rewrite systems.

Defining a Landauer embedding in order to make a computation mechanism reversible has been applied in different contexts and computational models, e.g., a probabilistic guarded command language [44], a low level virtual machine [35], the call-by-name lambda calculus [19, 21], cellular automata [38, 27], combinatory logic [11], a flowchart language [41], etc.

In the context of declarative languages, we find the work by Mu et al. [29], where a relational reversible language is presented (in the context of bidirectional programming). A similar approach was then introduced by Matsuda et al. [24, 25] in the context of functional programs and bidirectional transformation. The functional programs considered in [24] can be seen as linear and right-treeless constructor TRSs. The class of functional programs is more general in [25], which would correspond to left-linear, right-treeless TRSs. The reversibilization technique of [24, 25] includes both an injectivization stage (by introducing a view complement function) and an inversion stage. These methods are closely related to the transformations of injectivization and inversion that we have presented in Section 5, although we developed them from a rather different starting point. Moreover, their methods for injectivization and inversion consider a more restricted class of systems than those considered in this paper. On the other hand, they apply a number of analyses to improve the result, which explains the smaller traces in their approach. All in all, we consider that our approach gives better insights to understand the need for some of the requirements of the program transformations and the class of considered programs. For instance, most of our requirements come from the need to remove programs positions from the traces, as shown in Section 4.

Finally, [37] considers the reversible language RFUN. Similarly to Janus, computations in RFUN are reversible without the need of a Landauer embedding. The paper also presents a transformation from a simple (irreversible) functional language, FUN, to RFUN, in order to highlight how irreversibilities are handled in RFUN. The transformation has some similarities with both the approach of [24] and our improved transformation in Section 5.3; on the other hand, though, [37] also applies the Bennett trick [6] in order to avoid some unnecessary information.

8 Discussion and Future Work

In this paper, we have introduced a reversible extension of term rewriting. In order to keep our approach as general as possible, we have initially considered DCTRSs as input systems, and proved the soundness and reversibility of our extension of rewriting. Then, in order to introduce a reversibilization transformation for these systems, we have also presented a transformation from DCTRSs to pure constructor systems (pcDCTRSs) which is correct for constructor reduction. A further improvement is presented for injective functions, which may have a significant impact in memory usage in some cases. Finally, we have successfully applied our approach in the context of bidirectional program transformation.

We have developed a prototype implementation of the reversibilization transformations introduced in Section 5. The tool can read an input TRS file (format .trs [1]) and then it applies in a sequential way the following transformations: flattening, simplification of constructor conditions, injectivization, and inversion. The tool prints out the CTRSs obtained at each transformation step. It is publicly available through a web interface from http://kaz.dsic.upv.es/rev-rewriting.html, where we have included a number of examples to easily test the tool.

As for future work, we plan to investigate new methods to further reduce the size of the traces. In particular, we find it interesting to define a reachability analysis for DCTRSs. A reachability analysis for CTRSs without extra-variables (1-CTRSs) can be found in [12], but the extension to deal with extra-variables in DCTRSs (since a DCTRS is a particular case of 3-CTRS) seems challenging. Furthermore, as mentioned in the paper, a completion procedure to add default cases to some functions (as suggested in Section 5.1) may help to broaden the applicability of the technique and avoid the restriction to constructor reduction. Finally, our injectivization and inversion transformations are correct w.r.t. innermost reduction. Extending our results to a lazy strategy is also an interesting topic for further research.

Acknowledgements

We thank the anonymous reviewers for their useful comments and suggestions to improve this paper.